Theorem mp3an23 1453

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  sbciegf  3816  predeq1  6302  wrecseq1  8302  ac6sfi  9286  unfilem1  9309  ordtypelem2  9513  infxpenc2  10016  dju0en  10169  cfsmolem  10264  axdc4lem  10449  1nqenq  10956  mul02lem1  11389  muleqadd  11857  halfcl  12436  rehalfcl  12437  half0  12438  2halves  12439  halfpos2  12440  halfnneg2  12442  halfaddsub  12444  nneo  12645  zeo  12647  peano5uzi  12650  fztp  13556  uzrdgxfr  13931  bcn2  14278  bcpasc  14280  hashxplem  14392  hashfun  14396  swrds2  14890  repsw2  14900  repsw3  14901  imre  15054  reim  15055  crim  15061  addcj  15094  imval2  15097  cnpart  15186  01sqrexlem7  15194  absmax  15275  binomfallfaclem2  15983  bpoly2  16000  bpoly3  16001  fsumcube  16003  efgt0  16045  sinf  16066  efi4p  16079  resin4p  16080  recos4p  16081  sinneg  16088  efival  16094  cosadd  16107  sinmul  16114  sinbnd  16122  cosbnd  16123  ef01bndlem  16126  sin01bnd  16127  cos01bnd  16128  sin01gt0  16132  cos01gt0  16133  sin02gt0  16134  rpnnen2lem11  16166  rpnnen2lem12  16167  odd2np1lem  16282  odd2np1  16283  pythagtriplem12  16758  pythagtriplem14  16760  pythagtriplem15  16761  pythagtriplem16  16762  pythagtriplem17  16763  pockthi  16839  prmreclem5  16852  prmreclem6  16853  prmlem0  17038  prdsplusg  17403  prdsmulr  17404  prdsvsca  17405  odinf  19430  lbsexg  20776  psgnghm2  21133  mopnex  24027  tngnm  24167  tngngp2  24168  tngngpd  24169  tngngp  24170  addccncf  24432  sub1cncf  24434  sub2cncf  24435  iihalf1  24446  iihalf2  24448  pjthlem1  24953  ovolunlem1a  25012  ovolunlem1  25013  opnmbllem  25117  vitalilem4  25127  iblcnlem1  25304  itgcnlem  25306  dvmptre  25485  dvmptim  25486  dvlipcn  25510  mdegldg  25583  aaliou3lem3  25856  aaliou3lem8  25857  sincosq1lem  26006  sincosq2sgn  26008  sincosq3sgn  26009  sincosq4sgn  26010  sinq12gt0  26016  abssinper  26029  coskpi  26031  sineq0  26032  coseq1  26033  efeq1  26036  resinf1o  26044  efif1olem2  26051  efif1olem4  26053  logneg2  26122  cxpsqrtlem  26209  cxpsqrt  26210  logsqrt  26211  1cubr  26344  leibpilem2  26443  basellem3  26584  ppiub  26704  chtublem  26711  chtub  26712  bcmax  26778  bcp1ctr  26779  bposlem2  26785  bposlem6  26789  bposlem9  26792  logdivsum  27033  mulscl  27587  4ipval2  29956  ipidsq  29958  dipcl  29960  dipcj  29962  ipasslem11  30088  hvmul0  30272  pjhthlem1  30639  h1de2bi  30802  spanunsni  30827  adjeu  31137  nmopge0  31159  nmfnge0  31175  opsqrlem6  31393  mdsl1i  31569  mdsl2bi  31571  mdexchi  31583  superpos  31602  atabsi  31649  dmdbr5ati  31670  cdj3lem1  31682  fpwrelmapffslem  31952  dp2cl  32041  dpfrac1  32053  cshw1s2  32119  ogrpaddlt  32230  ofldlt1  32426  ofldchr  32427  oddpwdc  33348  eulerpartgbij  33366  subfacp1lem2a  34166  subfacp1lem5  34170  subfacp1lem6  34171  subfaclim  34174  sinccvglem  34652  dfon2lem3  34752  dfon2lem7  34756  wsuceq1  34782  clsun  35208  vtoclefex  36210  finxpreclem5  36271  sin2h  36473  cos2h  36474  tan2h  36475  poimirlem22  36505  poimirlem31  36514  opnmbllem0  36519  mblfinlem3  36522  itg2addnclem3  36536  ftc1cnnclem  36554  ftc1anclem6  36561  ftc2nc  36565  dvasin  36567  fdc  36608  constcncf  36625  heiborlem7  36680  atlatmstc  38184  lcmineqlem10  40898  lcmineqlem12  40900  facp2  40954  fac2xp3  41015  sn-00idlem1  41272  0prjspnlem  41366  diophren  41541  oaabsb  42034  dftrcl3  42461  dfrtrcl3  42474  cotrclrcl  42483  lhe4.4ex1a  43078  dirkerper  44802  zlmodzxznm  47168  sinh-conventional  47774