Theorem mp3an23 1476

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

Syntax hints:   → wi 4   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  sbciegf  3784  predeq1  6292  wrecseq1  8298  ac6sfi  9230  unfilem1  9251  fiint  9273  ordtypelem2  9469  infxpenc2  9980  dju0en  10134  cfsmolem  10229  axdc4lem  10414  1nqenq  10922  mul02lem1  11361  muleqadd  11833  2halves  12441  halfcl  12449  rehalfcl  12450  half0  12451  halfpos2  12452  halfnneg2  12454  halfaddsub  12456  nneo  12659  zeo  12661  peano5uzi  12664  fztp  13587  uzrdgxfr  13982  bcn2  14334  bcpasc  14336  hashxplem  14448  hashfun  14452  swrds2  14955  repsw2  14965  repsw3  14966  imre  15137  reim  15138  crim  15144  addcj  15177  imval2  15180  cnpart  15269  01sqrexlem7  15277  absmax  15359  binomfallfaclem2  16072  bpoly2  16089  bpoly3  16090  fsumcube  16092  efgt0  16137  sinf  16158  efi4p  16171  resin4p  16172  recos4p  16173  sinneg  16180  efival  16186  cosadd  16199  sinmul  16206  sinbnd  16214  cosbnd  16215  ef01bndlem  16218  sin01bnd  16219  cos01bnd  16220  sin01gt0  16224  cos01gt0  16225  sin02gt0  16226  rpnnen2lem11  16258  rpnnen2lem12  16259  odd2np1lem  16376  odd2np1  16377  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem15  16867  pythagtriplem16  16868  pythagtriplem17  16869  pockthi  16945  prmreclem5  16958  prmreclem6  16959  prmlem0  17143  prdsplusg  17489  prdsmulr  17490  prdsvsca  17491  isghm  19258  odinf  19605  ogrpaddlt  20180  ofldlt1  20926  lbsexg  21236  ofldchr  21630  psgnghm2  21635  mopnex  24581  tngnm  24713  tngngp2  24714  tngngpd  24715  tngngp  24716  addccncf  24981  sub1cncf  24983  sub2cncf  24984  iihalf1  24995  iihalf2  24997  pjthlem1  25501  ovolunlem1a  25560  ovolunlem1  25561  opnmbllem  25665  vitalilem4  25675  iblcnlem1  25852  itgcnlem  25854  dvmptre  26033  dvmptim  26034  dvlipcn  26058  mdegldg  26128  aaliou3lem3  26410  aaliou3lem8  26411  sincosq1lem  26564  sincosq2sgn  26566  sincosq3sgn  26567  sincosq4sgn  26568  sinq12gt0  26574  abssinper  26588  coskpi  26590  sineq0  26591  coseq1  26592  efeq1  26595  resinf1o  26603  efif1olem2  26610  efif1olem4  26612  logneg2  26682  cxpsqrtlem  26769  cxpsqrt  26770  logsqrt  26771  1cubr  26909  leibpilem2  27008  basellem3  27149  ppiub  27270  chtublem  27277  chtub  27278  bcmax  27344  bcp1ctr  27345  bposlem2  27351  bposlem6  27355  bposlem9  27358  logdivsum  27599  elno  27712  mulscl  28229  4ipval2  30913  ipidsq  30915  dipcl  30917  dipcj  30919  ipasslem11  31045  hvmul0  31229  pjhthlem1  31596  h1de2bi  31759  spanunsni  31784  adjeu  32094  nmopge0  32116  nmfnge0  32132  opsqrlem6  32350  mdsl1i  32526  mdsl2bi  32528  mdexchi  32540  superpos  32559  atabsi  32606  dmdbr5ati  32627  cdj3lem1  32639  fpwrelmapffslem  32936  dp2cl  33059  dpfrac1  33071  cshw1s2  33140  oddpwdc  34653  eulerpartgbij  34671  subfacp1lem2a  35535  subfacp1lem5  35539  subfacp1lem6  35540  subfaclim  35543  sinccvglem  36027  dfon2lem3  36138  dfon2lem7  36142  wsuceq1  36168  clsun  36693  vtoclefex  37833  finxpreclem5  37894  sin2h  38114  cos2h  38115  tan2h  38116  poimirlem22  38146  poimirlem31  38155  opnmbllem0  38160  mblfinlem3  38163  itg2addnclem3  38177  ftc1cnnclem  38195  ftc1anclem6  38202  ftc2nc  38206  dvasin  38208  fdc  38249  constcncf  38266  heiborlem7  38321  atlatmstc  39948  lcmineqlem10  42660  lcmineqlem12  42662  facp2  42765  3rdpwhole  42906  sn-00idlem1  43012  0prjspnlem  43210  sn-isghm  43260  diophren  43395  oaabsb  43876  dftrcl3  44301  dfrtrcl3  44314  cotrclrcl  44323  lhe4.4ex1a  44910  dirkerper  46675  sinnpoly  47490  zlmodzxznm  49124  sinh-conventional  50365