Theorem mp3an23 1483

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 1480	. 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  3780  predeq1  6321  wrecseq1  8358  ac6sfi  9300  unfilem1  9322  fiint  9343  ordtypelem2  9537  infxpenc2  10125  dju0en  10278  cfsmolem  10372  axdc4lem  10557  1nqenq  11071  mul02lem1  11510  muleqadd  11984  2halves  12588  halfcl  12596  rehalfcl  12597  half0  12598  halfpos2  12599  halfnneg2  12601  halfaddsub  12603  nneo  12807  zeo  12809  peano5uzi  12812  fztp  13738  uzrdgxfr  14134  bcn2  14487  bcpasc  14489  hashxplem  14602  hashfun  14606  swrds2  15117  repsw2  15129  repsw3  15130  imre  15301  reim  15302  crim  15308  addcj  15341  imval2  15344  cnpart  15433  01sqrexlem7  15441  absmax  15523  binomfallfaclem2  16232  bpoly2  16249  bpoly3  16250  fsumcube  16252  efgt0  16297  sinf  16318  efi4p  16331  resin4p  16332  recos4p  16333  sinneg  16340  efival  16346  cosadd  16359  sinmul  16366  sinbnd  16374  cosbnd  16375  ef01bndlem  16378  sin01bnd  16379  cos01bnd  16380  sin01gt0  16384  cos01gt0  16385  sin02gt0  16386  rpnnen2lem11  16418  rpnnen2lem12  16419  odd2np1lem  16536  odd2np1  16537  pythagtriplem12  17030  pythagtriplem14  17032  pythagtriplem15  17033  pythagtriplem16  17034  pythagtriplem17  17035  pockthi  17111  prmreclem5  17124  prmreclem6  17125  prmlem0  17309  prdsplusg  17655  prdsmulr  17656  prdsvsca  17657  isghm  19456  odinf  19804  ogrpaddlt  20379  ofldlt1  21159  lbsexg  21469  ofldchr  21909  psgnghm2  21914  mopnex  24865  tngnm  24997  tngngp2  24998  tngngpd  24999  tngngp  25000  addccncf  25265  sub1cncf  25267  sub2cncf  25268  iihalf1  25279  iihalf2  25281  pjthlem1  25785  ovolunlem1a  25844  ovolunlem1  25845  opnmbllem  25949  vitalilem4  25959  iblcnlem1  26135  itgcnlem  26137  dvmptre  26316  dvmptim  26317  dvlipcn  26341  mdegldg  26411  aaliou3lem3  26698  aaliou3lem8  26699  sincosq1lem  26853  sincosq2sgn  26855  sincosq3sgn  26856  sincosq4sgn  26857  sinq12gt0  26863  abssinper  26876  coskpi  26878  sineq0  26879  coseq1  26880  efeq1  26883  resinf1o  26891  efif1olem2  26898  efif1olem4  26900  logneg2  26970  cxpsqrtlem  27057  cxpsqrt  27058  logsqrt  27059  1cubr  27197  leibpilem2  27296  basellem3  27437  ppiub  27558  chtublem  27565  chtub  27566  bcmax  27632  bcp1ctr  27633  bposlem2  27639  bposlem6  27643  bposlem9  27646  logdivsum  27887  elno  28030  mulscl  28547  4ipval2  31337  ipidsq  31339  dipcl  31341  dipcj  31343  ipasslem11  31469  hvmul0  31653  pjhthlem1  32020  h1de2bi  32183  spanunsni  32208  adjeu  32518  nmopge0  32540  nmfnge0  32556  opsqrlem6  32774  mdsl1i  32950  mdsl2bi  32952  mdexchi  32964  superpos  32983  atabsi  33030  dmdbr5ati  33051  cdj3lem1  33063  fpwrelmapffslem  33391  dp2cl  33513  dpfrac1  33525  cshw1s2  33588  oddpwdc  35053  eulerpartgbij  35071  subfacp1lem2a  36111  subfacp1lem5  36115  subfacp1lem6  36116  subfaclim  36119  sinccvglem  36603  dfon2lem3  36724  dfon2lem7  36728  wsuceq1  36754  clsun  37293  vtoclefex  38448  finxpreclem5  38509  sin2h  38724  cos2h  38725  tan2h  38726  poimirlem22  38751  poimirlem31  38760  opnmbllem0  38765  mblfinlem3  38768  itg2addnclem3  38782  ftc1cnnclem  38800  ftc1anclem6  38807  ftc2nc  38811  dvasin  38813  fdc  38870  constcncf  38887  heiborlem7  38942  atlatmstc  40567  lcmineqlem10  43279  lcmineqlem12  43281  facp2  43384  3rdpwhole  43540  sn-00idlem1  43640  0prjspnlem  43853  sn-isghm  43875  diophren  44011  oaabsb  44486  dftrcl3  44910  dfrtrcl3  44923  cotrclrcl  44932  lhe4.4ex1a  45503  grpgimcanon  46121  dirkerper  47309  sinnpoly  48144  zlmodzxznm  49812  sinh-conventional  51110