Theorem mp3an23 1452

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  sbciegf  3759  predeq1  6202  wrecseq1  8123  ac6sfi  9034  unfilem1  9054  ordtypelem2  9254  infxpenc2  9777  dju0en  9930  cfsmolem  10025  axdc4lem  10210  1nqenq  10717  mul02lem1  11149  muleqadd  11617  halfcl  12196  rehalfcl  12197  half0  12198  2halves  12199  halfpos2  12200  halfnneg2  12202  halfaddsub  12204  nneo  12402  zeo  12404  peano5uzi  12407  fztp  13309  uzrdgxfr  13683  bcn2  14029  bcpasc  14031  hashxplem  14144  hashfun  14148  swrds2  14649  repsw2  14659  repsw3  14660  imre  14815  reim  14816  crim  14822  addcj  14855  imval2  14858  cnpart  14947  sqrlem7  14956  absmax  15037  binomfallfaclem2  15746  bpoly2  15763  bpoly3  15764  fsumcube  15766  efgt0  15808  sinf  15829  efi4p  15842  resin4p  15843  recos4p  15844  sinneg  15851  efival  15857  cosadd  15870  sinmul  15877  sinbnd  15885  cosbnd  15886  ef01bndlem  15889  sin01bnd  15890  cos01bnd  15891  sin01gt0  15895  cos01gt0  15896  sin02gt0  15897  rpnnen2lem11  15929  rpnnen2lem12  15930  odd2np1lem  16045  odd2np1  16046  pythagtriplem12  16523  pythagtriplem14  16525  pythagtriplem15  16526  pythagtriplem16  16527  pythagtriplem17  16528  pockthi  16604  prmreclem5  16617  prmreclem6  16618  prmlem0  16803  prdsplusg  17165  prdsmulr  17166  prdsvsca  17167  odinf  19166  lbsexg  20422  psgnghm2  20782  mopnex  23671  tngnm  23811  tngngp2  23812  tngngpd  23813  tngngp  23814  addccncf  24076  sub1cncf  24078  sub2cncf  24079  iihalf1  24090  iihalf2  24092  pjthlem1  24597  ovolunlem1a  24656  ovolunlem1  24657  opnmbllem  24761  vitalilem4  24771  iblcnlem1  24948  itgcnlem  24950  dvmptre  25129  dvmptim  25130  dvlipcn  25154  mdegldg  25227  aaliou3lem3  25500  aaliou3lem8  25501  sincosq1lem  25650  sincosq2sgn  25652  sincosq3sgn  25653  sincosq4sgn  25654  sinq12gt0  25660  abssinper  25673  coskpi  25675  sineq0  25676  coseq1  25677  efeq1  25680  resinf1o  25688  efif1olem2  25695  efif1olem4  25697  logneg2  25766  cxpsqrtlem  25853  cxpsqrt  25854  logsqrt  25855  1cubr  25988  leibpilem2  26087  basellem3  26228  ppiub  26348  chtublem  26355  chtub  26356  bcmax  26422  bcp1ctr  26423  bposlem2  26429  bposlem6  26433  bposlem9  26436  logdivsum  26677  4ipval2  29064  ipidsq  29066  dipcl  29068  dipcj  29070  ipasslem11  29196  hvmul0  29380  pjhthlem1  29747  h1de2bi  29910  spanunsni  29935  adjeu  30245  nmopge0  30267  nmfnge0  30283  opsqrlem6  30501  mdsl1i  30677  mdsl2bi  30679  mdexchi  30691  superpos  30710  atabsi  30757  dmdbr5ati  30778  cdj3lem1  30790  fpwrelmapffslem  31061  dp2cl  31148  dpfrac1  31160  cshw1s2  31226  ogrpaddlt  31337  ofldlt1  31506  ofldchr  31507  oddpwdc  32315  eulerpartgbij  32333  subfacp1lem2a  33136  subfacp1lem5  33140  subfacp1lem6  33141  subfaclim  33144  sinccvglem  33624  dfon2lem3  33755  dfon2lem7  33759  wsuceq1  33803  clsun  34511  vtoclefex  35499  finxpreclem5  35560  sin2h  35761  cos2h  35762  tan2h  35763  poimirlem22  35793  poimirlem31  35802  opnmbllem0  35807  mblfinlem3  35810  itg2addnclem3  35824  ftc1cnnclem  35842  ftc1anclem6  35849  ftc2nc  35853  dvasin  35855  fdc  35897  constcncf  35914  heiborlem7  35969  atlatmstc  37327  lcmineqlem10  40041  lcmineqlem12  40043  facp2  40094  fac2xp3  40155  sn-00idlem1  40376  0prjspnlem  40455  diophren  40630  dftrcl3  41296  dfrtrcl3  41309  cotrclrcl  41318  lhe4.4ex1a  41915  dirkerper  43606  zlmodzxznm  45805  sinh-conventional  46408