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 690	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 207  df-an 396  df-3an 1089

This theorem is referenced by:  sbciegf  3844  predeq1  6334  wrecseq1  8359  ac6sfi  9348  unfilem1  9371  fiint  9394  ordtypelem2  9588  infxpenc2  10091  dju0en  10245  cfsmolem  10339  axdc4lem  10524  1nqenq  11031  mul02lem1  11466  muleqadd  11934  halfcl  12518  rehalfcl  12519  half0  12520  2halves  12521  halfpos2  12522  halfnneg2  12524  halfaddsub  12526  nneo  12727  zeo  12729  peano5uzi  12732  fztp  13640  uzrdgxfr  14018  bcn2  14368  bcpasc  14370  hashxplem  14482  hashfun  14486  swrds2  14989  repsw2  14999  repsw3  15000  imre  15157  reim  15158  crim  15164  addcj  15197  imval2  15200  cnpart  15289  01sqrexlem7  15297  absmax  15378  binomfallfaclem2  16088  bpoly2  16105  bpoly3  16106  fsumcube  16108  efgt0  16151  sinf  16172  efi4p  16185  resin4p  16186  recos4p  16187  sinneg  16194  efival  16200  cosadd  16213  sinmul  16220  sinbnd  16228  cosbnd  16229  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  sin01gt0  16238  cos01gt0  16239  sin02gt0  16240  rpnnen2lem11  16272  rpnnen2lem12  16273  odd2np1lem  16388  odd2np1  16389  pythagtriplem12  16873  pythagtriplem14  16875  pythagtriplem15  16876  pythagtriplem16  16877  pythagtriplem17  16878  pockthi  16954  prmreclem5  16967  prmreclem6  16968  prmlem0  17153  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  isghm  19255  odinf  19605  lbsexg  21189  psgnghm2  21622  mopnex  24553  tngnm  24693  tngngp2  24694  tngngpd  24695  tngngp  24696  addccncf  24962  sub1cncf  24964  sub2cncf  24965  iihalf1  24977  iihalf2  24980  pjthlem1  25490  ovolunlem1a  25550  ovolunlem1  25551  opnmbllem  25655  vitalilem4  25665  iblcnlem1  25843  itgcnlem  25845  dvmptre  26027  dvmptim  26028  dvlipcn  26053  mdegldg  26125  aaliou3lem3  26404  aaliou3lem8  26405  sincosq1lem  26557  sincosq2sgn  26559  sincosq3sgn  26560  sincosq4sgn  26561  sinq12gt0  26567  abssinper  26581  coskpi  26583  sineq0  26584  coseq1  26585  efeq1  26588  resinf1o  26596  efif1olem2  26603  efif1olem4  26605  logneg2  26675  cxpsqrtlem  26762  cxpsqrt  26763  logsqrt  26764  1cubr  26903  leibpilem2  27002  basellem3  27144  ppiub  27266  chtublem  27273  chtub  27274  bcmax  27340  bcp1ctr  27341  bposlem2  27347  bposlem6  27351  bposlem9  27354  logdivsum  27595  elno  27708  mulscl  28178  4ipval2  30740  ipidsq  30742  dipcl  30744  dipcj  30746  ipasslem11  30872  hvmul0  31056  pjhthlem1  31423  h1de2bi  31586  spanunsni  31611  adjeu  31921  nmopge0  31943  nmfnge0  31959  opsqrlem6  32177  mdsl1i  32353  mdsl2bi  32355  mdexchi  32367  superpos  32386  atabsi  32433  dmdbr5ati  32454  cdj3lem1  32466  fpwrelmapffslem  32746  dp2cl  32844  dpfrac1  32856  cshw1s2  32927  ogrpaddlt  33067  ofldlt1  33308  ofldchr  33309  oddpwdc  34319  eulerpartgbij  34337  subfacp1lem2a  35148  subfacp1lem5  35152  subfacp1lem6  35153  subfaclim  35156  sinccvglem  35640  dfon2lem3  35749  dfon2lem7  35753  wsuceq1  35779  clsun  36294  vtoclefex  37300  finxpreclem5  37361  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem22  37602  poimirlem31  37611  opnmbllem0  37616  mblfinlem3  37619  itg2addnclem3  37633  ftc1cnnclem  37651  ftc1anclem6  37658  ftc2nc  37662  dvasin  37664  fdc  37705  constcncf  37722  heiborlem7  37777  atlatmstc  39275  lcmineqlem10  41995  lcmineqlem12  41997  facp2  42100  fac2xp3  42196  sn-00idlem1  42374  0prjspnlem  42578  sn-isghm  42628  diophren  42769  oaabsb  43256  dftrcl3  43682  dfrtrcl3  43695  cotrclrcl  43704  lhe4.4ex1a  44298  dirkerper  46017  zlmodzxznm  48226  sinh-conventional  48831