Theorem mp3an23 1451

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 1448	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 687	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  sbciegf  3750  predeq1  6193  wrecseq1  8105  ac6sfi  8988  unfilem1  9008  ordtypelem2  9208  infxpenc2  9709  dju0en  9862  cfsmolem  9957  axdc4lem  10142  1nqenq  10649  mul02lem1  11081  muleqadd  11549  halfcl  12128  rehalfcl  12129  half0  12130  2halves  12131  halfpos2  12132  halfnneg2  12134  halfaddsub  12136  nneo  12334  zeo  12336  peano5uzi  12339  fztp  13241  uzrdgxfr  13615  bcn2  13961  bcpasc  13963  hashxplem  14076  hashfun  14080  swrds2  14581  repsw2  14591  repsw3  14592  imre  14747  reim  14748  crim  14754  addcj  14787  imval2  14790  cnpart  14879  sqrlem7  14888  absmax  14969  binomfallfaclem2  15678  bpoly2  15695  bpoly3  15696  fsumcube  15698  efgt0  15740  sinf  15761  efi4p  15774  resin4p  15775  recos4p  15776  sinneg  15783  efival  15789  cosadd  15802  sinmul  15809  sinbnd  15817  cosbnd  15818  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  sin01gt0  15827  cos01gt0  15828  sin02gt0  15829  rpnnen2lem11  15861  rpnnen2lem12  15862  odd2np1lem  15977  odd2np1  15978  pythagtriplem12  16455  pythagtriplem14  16457  pythagtriplem15  16458  pythagtriplem16  16459  pythagtriplem17  16460  pockthi  16536  prmreclem5  16549  prmreclem6  16550  prmlem0  16735  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  odinf  19085  lbsexg  20341  psgnghm2  20698  mopnex  23581  tngnm  23721  tngngp2  23722  tngngpd  23723  tngngp  23724  addccncf  23986  sub1cncf  23988  sub2cncf  23989  iihalf1  24000  iihalf2  24002  pjthlem1  24506  ovolunlem1a  24565  ovolunlem1  24566  opnmbllem  24670  vitalilem4  24680  iblcnlem1  24857  itgcnlem  24859  dvmptre  25038  dvmptim  25039  dvlipcn  25063  mdegldg  25136  aaliou3lem3  25409  aaliou3lem8  25410  sincosq1lem  25559  sincosq2sgn  25561  sincosq3sgn  25562  sincosq4sgn  25563  sinq12gt0  25569  abssinper  25582  coskpi  25584  sineq0  25585  coseq1  25586  efeq1  25589  resinf1o  25597  efif1olem2  25604  efif1olem4  25606  logneg2  25675  cxpsqrtlem  25762  cxpsqrt  25763  logsqrt  25764  1cubr  25897  leibpilem2  25996  basellem3  26137  ppiub  26257  chtublem  26264  chtub  26265  bcmax  26331  bcp1ctr  26332  bposlem2  26338  bposlem6  26342  bposlem9  26345  logdivsum  26586  4ipval2  28971  ipidsq  28973  dipcl  28975  dipcj  28977  ipasslem11  29103  hvmul0  29287  pjhthlem1  29654  h1de2bi  29817  spanunsni  29842  adjeu  30152  nmopge0  30174  nmfnge0  30190  opsqrlem6  30408  mdsl1i  30584  mdsl2bi  30586  mdexchi  30598  superpos  30617  atabsi  30664  dmdbr5ati  30685  cdj3lem1  30697  fpwrelmapffslem  30969  dp2cl  31056  dpfrac1  31068  cshw1s2  31134  ogrpaddlt  31245  ofldlt1  31414  ofldchr  31415  oddpwdc  32221  eulerpartgbij  32239  subfacp1lem2a  33042  subfacp1lem5  33046  subfacp1lem6  33047  subfaclim  33050  sinccvglem  33530  dfon2lem3  33667  dfon2lem7  33671  wsuceq1  33736  clsun  34444  vtoclefex  35432  finxpreclem5  35493  sin2h  35694  cos2h  35695  tan2h  35696  poimirlem22  35726  poimirlem31  35735  opnmbllem0  35740  mblfinlem3  35743  itg2addnclem3  35757  ftc1cnnclem  35775  ftc1anclem6  35782  ftc2nc  35786  dvasin  35788  fdc  35830  constcncf  35847  heiborlem7  35902  atlatmstc  37260  lcmineqlem10  39974  lcmineqlem12  39976  facp2  40027  fac2xp3  40088  sn-00idlem1  40302  0prjspnlem  40381  diophren  40551  dftrcl3  41217  dfrtrcl3  41230  cotrclrcl  41239  lhe4.4ex1a  41836  dirkerper  43527  zlmodzxznm  45726  sinh-conventional  46327