Theorem mp3an23 1451

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  sbciegf  3815  predeq1  6301  wrecseq1  8305  ac6sfi  9289  unfilem1  9312  ordtypelem2  9516  infxpenc2  10019  dju0en  10172  cfsmolem  10267  axdc4lem  10452  1nqenq  10959  mul02lem1  11394  muleqadd  11862  halfcl  12441  rehalfcl  12442  half0  12443  2halves  12444  halfpos2  12445  halfnneg2  12447  halfaddsub  12449  nneo  12650  zeo  12652  peano5uzi  12655  fztp  13561  uzrdgxfr  13936  bcn2  14283  bcpasc  14285  hashxplem  14397  hashfun  14401  swrds2  14895  repsw2  14905  repsw3  14906  imre  15059  reim  15060  crim  15066  addcj  15099  imval2  15102  cnpart  15191  01sqrexlem7  15199  absmax  15280  binomfallfaclem2  15988  bpoly2  16005  bpoly3  16006  fsumcube  16008  efgt0  16050  sinf  16071  efi4p  16084  resin4p  16085  recos4p  16086  sinneg  16093  efival  16099  cosadd  16112  sinmul  16119  sinbnd  16127  cosbnd  16128  ef01bndlem  16131  sin01bnd  16132  cos01bnd  16133  sin01gt0  16137  cos01gt0  16138  sin02gt0  16139  rpnnen2lem11  16171  rpnnen2lem12  16172  odd2np1lem  16287  odd2np1  16288  pythagtriplem12  16763  pythagtriplem14  16765  pythagtriplem15  16766  pythagtriplem16  16767  pythagtriplem17  16768  pockthi  16844  prmreclem5  16857  prmreclem6  16858  prmlem0  17043  prdsplusg  17408  prdsmulr  17409  prdsvsca  17410  odinf  19472  lbsexg  20922  psgnghm2  21353  mopnex  24248  tngnm  24388  tngngp2  24389  tngngpd  24390  tngngp  24391  addccncf  24657  sub1cncf  24659  sub2cncf  24660  iihalf1  24672  iihalf2  24675  pjthlem1  25185  ovolunlem1a  25245  ovolunlem1  25246  opnmbllem  25350  vitalilem4  25360  iblcnlem1  25537  itgcnlem  25539  dvmptre  25721  dvmptim  25722  dvlipcn  25746  mdegldg  25819  aaliou3lem3  26093  aaliou3lem8  26094  sincosq1lem  26243  sincosq2sgn  26245  sincosq3sgn  26246  sincosq4sgn  26247  sinq12gt0  26253  abssinper  26266  coskpi  26268  sineq0  26269  coseq1  26270  efeq1  26273  resinf1o  26281  efif1olem2  26288  efif1olem4  26290  logneg2  26359  cxpsqrtlem  26446  cxpsqrt  26447  logsqrt  26448  1cubr  26583  leibpilem2  26682  basellem3  26823  ppiub  26943  chtublem  26950  chtub  26951  bcmax  27017  bcp1ctr  27018  bposlem2  27024  bposlem6  27028  bposlem9  27031  logdivsum  27272  mulscl  27829  4ipval2  30228  ipidsq  30230  dipcl  30232  dipcj  30234  ipasslem11  30360  hvmul0  30544  pjhthlem1  30911  h1de2bi  31074  spanunsni  31099  adjeu  31409  nmopge0  31431  nmfnge0  31447  opsqrlem6  31665  mdsl1i  31841  mdsl2bi  31843  mdexchi  31855  superpos  31874  atabsi  31921  dmdbr5ati  31942  cdj3lem1  31954  fpwrelmapffslem  32224  dp2cl  32313  dpfrac1  32325  cshw1s2  32391  ogrpaddlt  32505  ofldlt1  32701  ofldchr  32702  oddpwdc  33651  eulerpartgbij  33669  subfacp1lem2a  34469  subfacp1lem5  34473  subfacp1lem6  34474  subfaclim  34477  sinccvglem  34955  dfon2lem3  35061  dfon2lem7  35065  wsuceq1  35091  clsun  35516  vtoclefex  36518  finxpreclem5  36579  sin2h  36781  cos2h  36782  tan2h  36783  poimirlem22  36813  poimirlem31  36822  opnmbllem0  36827  mblfinlem3  36830  itg2addnclem3  36844  ftc1cnnclem  36862  ftc1anclem6  36869  ftc2nc  36873  dvasin  36875  fdc  36916  constcncf  36933  heiborlem7  36988  atlatmstc  38492  lcmineqlem10  41209  lcmineqlem12  41211  facp2  41265  fac2xp3  41326  sn-00idlem1  41573  0prjspnlem  41667  diophren  41853  oaabsb  42346  dftrcl3  42773  dfrtrcl3  42786  cotrclrcl  42795  lhe4.4ex1a  43390  dirkerper  45110  zlmodzxznm  47265  sinh-conventional  47871