Theorem mp3an23 1449

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 1446	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 689	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 206  df-an 395  df-3an 1086

This theorem is referenced by:  sbciegf  3813  predeq1  6309  wrecseq1  8324  ac6sfi  9312  unfilem1  9335  ordtypelem2  9544  infxpenc2  10047  dju0en  10200  cfsmolem  10295  axdc4lem  10480  1nqenq  10987  mul02lem1  11422  muleqadd  11890  halfcl  12470  rehalfcl  12471  half0  12472  2halves  12473  halfpos2  12474  halfnneg2  12476  halfaddsub  12478  nneo  12679  zeo  12681  peano5uzi  12684  fztp  13592  uzrdgxfr  13968  bcn2  14314  bcpasc  14316  hashxplem  14428  hashfun  14432  swrds2  14927  repsw2  14937  repsw3  14938  imre  15091  reim  15092  crim  15098  addcj  15131  imval2  15134  cnpart  15223  01sqrexlem7  15231  absmax  15312  binomfallfaclem2  16020  bpoly2  16037  bpoly3  16038  fsumcube  16040  efgt0  16083  sinf  16104  efi4p  16117  resin4p  16118  recos4p  16119  sinneg  16126  efival  16132  cosadd  16145  sinmul  16152  sinbnd  16160  cosbnd  16161  ef01bndlem  16164  sin01bnd  16165  cos01bnd  16166  sin01gt0  16170  cos01gt0  16171  sin02gt0  16172  rpnnen2lem11  16204  rpnnen2lem12  16205  odd2np1lem  16320  odd2np1  16321  pythagtriplem12  16798  pythagtriplem14  16800  pythagtriplem15  16801  pythagtriplem16  16802  pythagtriplem17  16803  pockthi  16879  prmreclem5  16892  prmreclem6  16893  prmlem0  17078  prdsplusg  17443  prdsmulr  17444  prdsvsca  17445  isghm  19178  odinf  19530  lbsexg  21064  psgnghm2  21530  mopnex  24472  tngnm  24612  tngngp2  24613  tngngpd  24614  tngngp  24615  addccncf  24881  sub1cncf  24883  sub2cncf  24884  iihalf1  24896  iihalf2  24899  pjthlem1  25409  ovolunlem1a  25469  ovolunlem1  25470  opnmbllem  25574  vitalilem4  25584  iblcnlem1  25761  itgcnlem  25763  dvmptre  25945  dvmptim  25946  dvlipcn  25971  mdegldg  26046  aaliou3lem3  26324  aaliou3lem8  26325  sincosq1lem  26477  sincosq2sgn  26479  sincosq3sgn  26480  sincosq4sgn  26481  sinq12gt0  26487  abssinper  26500  coskpi  26502  sineq0  26503  coseq1  26504  efeq1  26507  resinf1o  26515  efif1olem2  26522  efif1olem4  26524  logneg2  26594  cxpsqrtlem  26681  cxpsqrt  26682  logsqrt  26683  1cubr  26819  leibpilem2  26918  basellem3  27060  ppiub  27182  chtublem  27189  chtub  27190  bcmax  27256  bcp1ctr  27257  bposlem2  27263  bposlem6  27267  bposlem9  27270  logdivsum  27511  elno  27624  mulscl  28084  4ipval2  30590  ipidsq  30592  dipcl  30594  dipcj  30596  ipasslem11  30722  hvmul0  30906  pjhthlem1  31273  h1de2bi  31436  spanunsni  31461  adjeu  31771  nmopge0  31793  nmfnge0  31809  opsqrlem6  32027  mdsl1i  32203  mdsl2bi  32205  mdexchi  32217  superpos  32236  atabsi  32283  dmdbr5ati  32304  cdj3lem1  32316  fpwrelmapffslem  32596  dp2cl  32688  dpfrac1  32700  cshw1s2  32770  ogrpaddlt  32887  ofldlt1  33127  ofldchr  33128  oddpwdc  34105  eulerpartgbij  34123  subfacp1lem2a  34921  subfacp1lem5  34925  subfacp1lem6  34926  subfaclim  34929  sinccvglem  35407  dfon2lem3  35512  dfon2lem7  35516  wsuceq1  35542  clsun  35943  vtoclefex  36944  finxpreclem5  37005  sin2h  37214  cos2h  37215  tan2h  37216  poimirlem22  37246  poimirlem31  37255  opnmbllem0  37260  mblfinlem3  37263  itg2addnclem3  37277  ftc1cnnclem  37295  ftc1anclem6  37302  ftc2nc  37306  dvasin  37308  fdc  37349  constcncf  37366  heiborlem7  37421  atlatmstc  38921  lcmineqlem10  41641  lcmineqlem12  41643  facp2  41746  fac2xp3  41825  sn-00idlem1  42088  0prjspnlem  42182  sn-isghm  42232  diophren  42375  oaabsb  42865  dftrcl3  43292  dfrtrcl3  43305  cotrclrcl  43314  lhe4.4ex1a  43908  dirkerper  45622  zlmodzxznm  47751  sinh-conventional  48356