Theorem mp3an23 1581

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

Syntax hints:   → wi 4   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  sbciegf  3694  predeq1  5926  wrecseq1  7680  ac6sfi  8479  unfilem1  8499  ordtypelem2  8700  infxpenc2  9165  cda0en  9323  cfsmolem  9414  axdc4lem  9599  1nqenq  10106  mul02lem1  10538  muleqadd  11003  halfcl  11590  rehalfcl  11591  half0  11592  2halves  11593  halfpos2  11594  halfnneg2  11596  halfaddsub  11598  nneo  11796  zeo  11798  peano5uzi  11801  fztp  12697  uzrdgxfr  13068  bcn2  13406  bcpasc  13408  hashxplem  13516  hashfun  13520  swrds2  14068  repsw2  14078  repsw3  14079  imre  14232  reim  14233  crim  14239  addcj  14272  imval2  14275  cnpart  14364  sqrlem7  14373  absmax  14453  binomfallfaclem2  15150  bpoly2  15167  bpoly3  15168  fsumcube  15170  efgt0  15212  sinf  15233  efi4p  15246  resin4p  15247  recos4p  15248  sinneg  15255  efival  15261  cosadd  15274  sinmul  15281  sinbnd  15289  cosbnd  15290  ef01bndlem  15293  sin01bnd  15294  cos01bnd  15295  sin01gt0  15299  cos01gt0  15300  sin02gt0  15301  rpnnen2lem11  15334  rpnnen2lem12  15335  odd2np1lem  15445  odd2np1  15446  pythagtriplem12  15909  pythagtriplem14  15911  pythagtriplem15  15912  pythagtriplem16  15913  pythagtriplem17  15914  pockthi  15989  prmreclem5  16002  prmreclem6  16003  prmlem0  16185  prdsplusg  16478  prdsmulr  16479  prdsvsca  16480  odinf  18338  lbsexg  19532  psgnghm2  20293  mopnex  22701  tngnm  22832  tngngp2  22833  tngngpd  22834  tngngp  22835  addccncf  23096  iihalf1  23107  iihalf2  23109  pjthlem1  23612  ovolunlem1a  23669  ovolunlem1  23670  opnmbllem  23774  vitalilem4  23784  iblcnlem1  23960  itgcnlem  23962  dvmptre  24138  dvmptim  24139  dvlipcn  24163  mdegldg  24232  aaliou3lem3  24505  aaliou3lem8  24506  sincosq1lem  24656  sincosq2sgn  24658  sincosq3sgn  24659  sincosq4sgn  24660  sinq12gt0  24666  abssinper  24677  coskpi  24679  sineq0  24680  coseq1  24681  efeq1  24682  resinf1o  24689  efif1olem2  24696  efif1olem4  24698  logneg2  24767  cxpsqrtlem  24854  cxpsqrt  24855  logsqrt  24856  1cubr  24989  leibpilem1  25087  leibpilem2  25088  basellem3  25229  ppiub  25349  chtublem  25356  chtub  25357  bcmax  25423  bcp1ctr  25424  bposlem2  25430  bposlem6  25434  bposlem9  25437  logdivsum  25642  4ipval2  28114  ipidsq  28116  dipcl  28118  dipcj  28120  ipasslem11  28246  hvmul0  28432  pjhthlem1  28801  h1de2bi  28964  spanunsni  28989  adjeu  29299  nmopge0  29321  nmfnge0  29337  opsqrlem6  29555  mdsl1i  29731  mdsl2bi  29733  mdexchi  29745  superpos  29764  atabsi  29811  dmdbr5ati  29832  cdj3lem1  29844  fpwrelmapffslem  30051  dp2cl  30129  dpfrac1  30141  ogrpaddlt  30259  ofldlt1  30354  ofldchr  30355  oddpwdc  30957  eulerpartgbij  30975  subfacp1lem2a  31704  subfacp1lem5  31708  subfacp1lem6  31709  subfaclim  31712  sinccvglem  32106  dfon2lem3  32223  dfon2lem7  32227  wsuceq1  32294  clsun  32856  vtoclefex  33722  finxpreclem5  33772  sin2h  33937  cos2h  33938  tan2h  33939  poimirlem22  33970  poimirlem31  33979  opnmbllem0  33984  mblfinlem3  33987  itg2addnclem3  34001  ftc1cnnclem  34021  ftc1anclem6  34028  ftc2nc  34032  dvasin  34034  fdc  34078  constcncf  34095  sub1cncf  34097  sub2cncf  34098  heiborlem7  34153  atlatmstc  35389  diophren  38216  dftrcl3  38848  dfrtrcl3  38861  cotrclrcl  38870  lhe4.4ex1a  39363  dirkerper  41101  zlmodzxznm  43147  sinh-conventional  43388