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 1083

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 399  df-3an 1085

This theorem is referenced by:  sbciegf  3809  predeq1  6150  wrecseq1  7950  ac6sfi  8762  unfilem1  8782  ordtypelem2  8983  infxpenc2  9448  dju0en  9601  cfsmolem  9692  axdc4lem  9877  1nqenq  10384  mul02lem1  10816  muleqadd  11284  halfcl  11863  rehalfcl  11864  half0  11865  2halves  11866  halfpos2  11867  halfnneg2  11869  halfaddsub  11871  nneo  12067  zeo  12069  peano5uzi  12072  fztp  12964  uzrdgxfr  13336  bcn2  13680  bcpasc  13682  hashxplem  13795  hashfun  13799  swrds2  14302  repsw2  14312  repsw3  14313  imre  14467  reim  14468  crim  14474  addcj  14507  imval2  14510  cnpart  14599  sqrlem7  14608  absmax  14689  binomfallfaclem2  15394  bpoly2  15411  bpoly3  15412  fsumcube  15414  efgt0  15456  sinf  15477  efi4p  15490  resin4p  15491  recos4p  15492  sinneg  15499  efival  15505  cosadd  15518  sinmul  15525  sinbnd  15533  cosbnd  15534  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  sin01gt0  15543  cos01gt0  15544  sin02gt0  15545  rpnnen2lem11  15577  rpnnen2lem12  15578  odd2np1lem  15689  odd2np1  15690  pythagtriplem12  16163  pythagtriplem14  16165  pythagtriplem15  16166  pythagtriplem16  16167  pythagtriplem17  16168  pockthi  16243  prmreclem5  16256  prmreclem6  16257  prmlem0  16439  prdsplusg  16731  prdsmulr  16732  prdsvsca  16733  odinf  18690  lbsexg  19936  psgnghm2  20725  mopnex  23129  tngnm  23260  tngngp2  23261  tngngpd  23262  tngngp  23263  addccncf  23524  iihalf1  23535  iihalf2  23537  pjthlem1  24040  ovolunlem1a  24097  ovolunlem1  24098  opnmbllem  24202  vitalilem4  24212  iblcnlem1  24388  itgcnlem  24390  dvmptre  24566  dvmptim  24567  dvlipcn  24591  mdegldg  24660  aaliou3lem3  24933  aaliou3lem8  24934  sincosq1lem  25083  sincosq2sgn  25085  sincosq3sgn  25086  sincosq4sgn  25087  sinq12gt0  25093  abssinper  25106  coskpi  25108  sineq0  25109  coseq1  25110  efeq1  25113  resinf1o  25120  efif1olem2  25127  efif1olem4  25129  logneg2  25198  cxpsqrtlem  25285  cxpsqrt  25286  logsqrt  25287  1cubr  25420  leibpilem2  25519  basellem3  25660  ppiub  25780  chtublem  25787  chtub  25788  bcmax  25854  bcp1ctr  25855  bposlem2  25861  bposlem6  25865  bposlem9  25868  logdivsum  26109  4ipval2  28485  ipidsq  28487  dipcl  28489  dipcj  28491  ipasslem11  28617  hvmul0  28801  pjhthlem1  29168  h1de2bi  29331  spanunsni  29356  adjeu  29666  nmopge0  29688  nmfnge0  29704  opsqrlem6  29922  mdsl1i  30098  mdsl2bi  30100  mdexchi  30112  superpos  30131  atabsi  30178  dmdbr5ati  30199  cdj3lem1  30211  fpwrelmapffslem  30468  dp2cl  30556  dpfrac1  30568  cshw1s2  30634  ogrpaddlt  30718  ofldlt1  30886  ofldchr  30887  oddpwdc  31612  eulerpartgbij  31630  subfacp1lem2a  32427  subfacp1lem5  32431  subfacp1lem6  32432  subfaclim  32435  sinccvglem  32915  dfon2lem3  33030  dfon2lem7  33034  wsuceq1  33102  clsun  33676  vtoclefex  34618  finxpreclem5  34679  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem22  34929  poimirlem31  34938  opnmbllem0  34943  mblfinlem3  34946  itg2addnclem3  34960  ftc1cnnclem  34980  ftc1anclem6  34987  ftc2nc  34991  dvasin  34993  fdc  35035  constcncf  35052  sub1cncf  35054  sub2cncf  35055  heiborlem7  35110  atlatmstc  36470  fac2xp3  39143  facp2  39144  sn-00idlem1  39277  0prjspnlem  39317  diophren  39459  dftrcl3  40114  dfrtrcl3  40127  cotrclrcl  40136  lhe4.4ex1a  40710  dirkerper  42430  zlmodzxznm  44601  sinh-conventional  44887