Theorem mp3an23 1450

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  sbciegf  3757  predeq1  6118  wrecseq1  7933  ac6sfi  8746  unfilem1  8766  ordtypelem2  8967  infxpenc2  9433  dju0en  9586  cfsmolem  9681  axdc4lem  9866  1nqenq  10373  mul02lem1  10805  muleqadd  11273  halfcl  11850  rehalfcl  11851  half0  11852  2halves  11853  halfpos2  11854  halfnneg2  11856  halfaddsub  11858  nneo  12054  zeo  12056  peano5uzi  12059  fztp  12958  uzrdgxfr  13330  bcn2  13675  bcpasc  13677  hashxplem  13790  hashfun  13794  swrds2  14293  repsw2  14303  repsw3  14304  imre  14459  reim  14460  crim  14466  addcj  14499  imval2  14502  cnpart  14591  sqrlem7  14600  absmax  14681  binomfallfaclem2  15386  bpoly2  15403  bpoly3  15404  fsumcube  15406  efgt0  15448  sinf  15469  efi4p  15482  resin4p  15483  recos4p  15484  sinneg  15491  efival  15497  cosadd  15510  sinmul  15517  sinbnd  15525  cosbnd  15526  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  sin01gt0  15535  cos01gt0  15536  sin02gt0  15537  rpnnen2lem11  15569  rpnnen2lem12  15570  odd2np1lem  15681  odd2np1  15682  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem15  16156  pythagtriplem16  16157  pythagtriplem17  16158  pockthi  16233  prmreclem5  16246  prmreclem6  16247  prmlem0  16431  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  odinf  18682  lbsexg  19929  psgnghm2  20270  mopnex  23126  tngnm  23257  tngngp2  23258  tngngpd  23259  tngngp  23260  addccncf  23522  sub1cncf  23524  sub2cncf  23525  iihalf1  23536  iihalf2  23538  pjthlem1  24041  ovolunlem1a  24100  ovolunlem1  24101  opnmbllem  24205  vitalilem4  24215  iblcnlem1  24391  itgcnlem  24393  dvmptre  24572  dvmptim  24573  dvlipcn  24597  mdegldg  24667  aaliou3lem3  24940  aaliou3lem8  24941  sincosq1lem  25090  sincosq2sgn  25092  sincosq3sgn  25093  sincosq4sgn  25094  sinq12gt0  25100  abssinper  25113  coskpi  25115  sineq0  25116  coseq1  25117  efeq1  25120  resinf1o  25128  efif1olem2  25135  efif1olem4  25137  logneg2  25206  cxpsqrtlem  25293  cxpsqrt  25294  logsqrt  25295  1cubr  25428  leibpilem2  25527  basellem3  25668  ppiub  25788  chtublem  25795  chtub  25796  bcmax  25862  bcp1ctr  25863  bposlem2  25869  bposlem6  25873  bposlem9  25876  logdivsum  26117  4ipval2  28491  ipidsq  28493  dipcl  28495  dipcj  28497  ipasslem11  28623  hvmul0  28807  pjhthlem1  29174  h1de2bi  29337  spanunsni  29362  adjeu  29672  nmopge0  29694  nmfnge0  29710  opsqrlem6  29928  mdsl1i  30104  mdsl2bi  30106  mdexchi  30118  superpos  30137  atabsi  30184  dmdbr5ati  30205  cdj3lem1  30217  fpwrelmapffslem  30494  dp2cl  30582  dpfrac1  30594  cshw1s2  30660  ogrpaddlt  30768  ofldlt1  30937  ofldchr  30938  oddpwdc  31722  eulerpartgbij  31740  subfacp1lem2a  32540  subfacp1lem5  32544  subfacp1lem6  32545  subfaclim  32548  sinccvglem  33028  dfon2lem3  33143  dfon2lem7  33147  wsuceq1  33215  clsun  33789  vtoclefex  34751  finxpreclem5  34812  sin2h  35047  cos2h  35048  tan2h  35049  poimirlem22  35079  poimirlem31  35088  opnmbllem0  35093  mblfinlem3  35096  itg2addnclem3  35110  ftc1cnnclem  35128  ftc1anclem6  35135  ftc2nc  35139  dvasin  35141  fdc  35183  constcncf  35200  heiborlem7  35255  atlatmstc  36615  lcmineqlem10  39326  lcmineqlem12  39328  facp2  39347  fac2xp3  39385  sn-00idlem1  39536  0prjspnlem  39612  diophren  39754  dftrcl3  40421  dfrtrcl3  40434  cotrclrcl  40443  lhe4.4ex1a  41033  dirkerper  42738  zlmodzxznm  44906  sinh-conventional  45265