Theorem mp3an23 1482

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  sbciegf  3776  predeq1  6306  wrecseq1  8333  ac6sfi  9275  unfilem1  9297  fiint  9318  ordtypelem2  9513  infxpenc2  10101  dju0en  10254  cfsmolem  10348  axdc4lem  10533  1nqenq  11047  mul02lem1  11486  muleqadd  11960  2halves  12564  halfcl  12572  rehalfcl  12573  half0  12574  halfpos2  12575  halfnneg2  12577  halfaddsub  12579  nneo  12783  zeo  12785  peano5uzi  12788  fztp  13714  uzrdgxfr  14110  bcn2  14463  bcpasc  14465  hashxplem  14578  hashfun  14582  swrds2  15091  repsw2  15103  repsw3  15104  imre  15275  reim  15276  crim  15282  addcj  15315  imval2  15318  cnpart  15407  01sqrexlem7  15415  absmax  15497  binomfallfaclem2  16206  bpoly2  16223  bpoly3  16224  fsumcube  16226  efgt0  16271  sinf  16292  efi4p  16305  resin4p  16306  recos4p  16307  sinneg  16314  efival  16320  cosadd  16333  sinmul  16340  sinbnd  16348  cosbnd  16349  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  sin01gt0  16358  cos01gt0  16359  sin02gt0  16360  rpnnen2lem11  16392  rpnnen2lem12  16393  odd2np1lem  16510  odd2np1  16511  pythagtriplem12  17004  pythagtriplem14  17006  pythagtriplem15  17007  pythagtriplem16  17008  pythagtriplem17  17009  pockthi  17085  prmreclem5  17098  prmreclem6  17099  prmlem0  17283  prdsplusg  17629  prdsmulr  17630  prdsvsca  17631  isghm  19430  odinf  19777  ogrpaddlt  20352  ofldlt1  21132  lbsexg  21442  ofldchr  21882  psgnghm2  21887  mopnex  24838  tngnm  24970  tngngp2  24971  tngngpd  24972  tngngp  24973  addccncf  25238  sub1cncf  25240  sub2cncf  25241  iihalf1  25252  iihalf2  25254  pjthlem1  25758  ovolunlem1a  25817  ovolunlem1  25818  opnmbllem  25922  vitalilem4  25932  iblcnlem1  26108  itgcnlem  26110  dvmptre  26289  dvmptim  26290  dvlipcn  26314  mdegldg  26384  aaliou3lem3  26671  aaliou3lem8  26672  sincosq1lem  26826  sincosq2sgn  26828  sincosq3sgn  26829  sincosq4sgn  26830  sinq12gt0  26836  abssinper  26849  coskpi  26851  sineq0  26852  coseq1  26853  efeq1  26856  resinf1o  26864  efif1olem2  26871  efif1olem4  26873  logneg2  26943  cxpsqrtlem  27030  cxpsqrt  27031  logsqrt  27032  1cubr  27170  leibpilem2  27269  basellem3  27410  ppiub  27531  chtublem  27538  chtub  27539  bcmax  27605  bcp1ctr  27606  bposlem2  27612  bposlem6  27616  bposlem9  27619  logdivsum  27860  elno  28003  mulscl  28520  4ipval2  31310  ipidsq  31312  dipcl  31314  dipcj  31316  ipasslem11  31442  hvmul0  31626  pjhthlem1  31993  h1de2bi  32156  spanunsni  32181  adjeu  32491  nmopge0  32513  nmfnge0  32529  opsqrlem6  32747  mdsl1i  32923  mdsl2bi  32925  mdexchi  32937  superpos  32956  atabsi  33003  dmdbr5ati  33024  cdj3lem1  33036  fpwrelmapffslem  33324  dp2cl  33446  dpfrac1  33458  cshw1s2  33521  oddpwdc  34986  eulerpartgbij  35004  subfacp1lem2a  35945  subfacp1lem5  35949  subfacp1lem6  35950  subfaclim  35953  sinccvglem  36437  dfon2lem3  36547  dfon2lem7  36551  wsuceq1  36577  clsun  37116  vtoclefex  38258  finxpreclem5  38319  sin2h  38534  cos2h  38535  tan2h  38536  poimirlem22  38561  poimirlem31  38570  opnmbllem0  38575  mblfinlem3  38578  itg2addnclem3  38592  ftc1cnnclem  38610  ftc1anclem6  38617  ftc2nc  38621  dvasin  38623  fdc  38680  constcncf  38697  heiborlem7  38752  atlatmstc  40377  lcmineqlem10  43089  lcmineqlem12  43091  facp2  43194  3rdpwhole  43350  sn-00idlem1  43450  0prjspnlem  43663  sn-isghm  43685  diophren  43820  oaabsb  44296  dftrcl3  44720  dfrtrcl3  44733  cotrclrcl  44742  lhe4.4ex1a  45313  dirkerper  47106  sinnpoly  47941  zlmodzxznm  49609  sinh-conventional  50832