Theorem mp3an23 1408

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	⊢ 𝜓
mp3an23.2	⊢ 𝜒
mp3an23.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an23	⊢ (𝜑 → 𝜃)

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 ⊢ 𝜓
2		mp3an23.2	. . 3 ⊢ 𝜒
3		mp3an23.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1405	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 703	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  sbciegf  3434  predeq1  5599  wrecseq1  7297  ac6sfi  8089  unfilem1  8109  ordtypelem2  8307  infxpenc2  8728  cda0en  8884  cfsmolem  8975  axdc4lem  9160  1nqenq  9663  mul02lem1  10091  muleqadd  10550  halfcl  11134  rehalfcl  11135  half0  11136  2halves  11137  halfpos2  11138  halfnneg2  11140  halfaddsub  11142  nneo  11337  zeo  11339  peano5uzi  11342  fztp  12267  uzrdgxfr  12628  bcn2  12968  bcpasc  12970  hashxplem  13080  hashfun  13084  swrds2  13533  repsw2  13541  repsw3  13542  imre  13696  reim  13697  crim  13703  addcj  13736  imval2  13739  cnpart  13828  sqrlem7  13837  absmax  13917  binomfallfaclem2  14610  bpoly2  14627  bpoly3  14628  fsumcube  14630  efgt0  14672  sinf  14693  efi4p  14706  resin4p  14707  recos4p  14708  sinneg  14715  efival  14721  cosadd  14734  sinmul  14741  sinbnd  14749  cosbnd  14750  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  sin01gt0  14759  cos01gt0  14760  sin02gt0  14761  rpnnen2lem11  14792  rpnnen2lem12  14793  odd2np1lem  14902  odd2np1  14903  pythagtriplem12  15369  pythagtriplem14  15371  pythagtriplem15  15372  pythagtriplem16  15373  pythagtriplem17  15374  pockthi  15449  prmreclem5  15462  prmreclem6  15463  prmlem0  15650  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  odinf  17803  lbsexg  18985  psgnghm2  19746  mopnex  22134  tngnm  22265  tngngp2  22266  tngngpd  22267  tngngp  22268  addccncf  22527  iihalf1  22538  iihalf2  22540  pjthlem1  23016  ovolunlem1a  23071  ovolunlem1  23072  opnmbllem  23175  vitalilem4  23186  iblcnlem1  23360  itgcnlem  23362  dvmptre  23538  dvmptim  23539  dvlipcn  23561  mdegldg  23630  aaliou3lem3  23903  aaliou3lem8  23904  sincosq1lem  24053  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  sinq12gt0  24063  abssinper  24074  coskpi  24076  sineq0  24077  coseq1  24078  efeq1  24079  resinf1o  24086  efif1olem2  24093  efif1olem4  24095  logneg2  24165  cxpsqrtlem  24248  cxpsqrt  24249  logsqrt  24250  1cubr  24369  leibpilem1  24467  leibpilem2  24468  basellem3  24609  ppiub  24729  chtublem  24736  chtub  24737  bcmax  24803  bcp1ctr  24804  bposlem2  24810  bposlem6  24814  bposlem9  24817  logdivsum  25022  4ipval2  26947  ipidsq  26949  dipcl  26951  dipcj  26953  ipasslem11  27079  hvmul0  27265  pjhthlem1  27634  h1de2bi  27797  spanunsni  27822  adjeu  28132  nmopge0  28154  nmfnge0  28170  opsqrlem6  28388  mdsl1i  28564  mdsl2bi  28566  mdexchi  28578  superpos  28597  atabsi  28644  dmdbr5ati  28665  cdj3lem1  28677  fpwrelmapffslem  28895  ogrpaddlt  29049  ofldlt1  29144  ofldchr  29145  oddpwdc  29743  eulerpartgbij  29761  subfacp1lem2a  30416  subfacp1lem5  30420  subfacp1lem6  30421  subfaclim  30424  sinccvglem  30820  dfon2lem3  30934  dfon2lem7  30938  wsuceq1  31005  clsun  31493  vtoclefex  32357  finxpreclem5  32408  sin2h  32569  cos2h  32570  tan2h  32571  poimirlem22  32601  poimirlem31  32610  opnmbllem0  32615  mblfinlem3  32618  itg2addnclem3  32633  ftc1cnnclem  32653  ftc1anclem6  32660  ftc2nc  32664  dvasin  32666  fdc  32711  constcncf  32728  sub1cncf  32730  sub2cncf  32731  heiborlem7  32786  atlatmstc  33624  diophren  36395  dftrcl3  37031  dfrtrcl3  37044  cotrclrcl  37053  lhe4.4ex1a  37550  dirkerper  38989  upgr1wlkcompim  40851  upgrtrls  40909  upgrspths1wlk  40944  zlmodzxznm  42080  sinh-conventional  42279  dp2cl  42309  dpfrac1  42312  dpfrac1OLD  42313