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 691	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  sbciegf  3830  predeq1  6324  wrecseq1  8341  ac6sfi  9317  unfilem1  9340  fiint  9363  ordtypelem2  9556  infxpenc2  10059  dju0en  10213  cfsmolem  10307  axdc4lem  10492  1nqenq  10999  mul02lem1  11434  muleqadd  11904  halfcl  12488  rehalfcl  12489  half0  12490  2halves  12491  halfpos2  12492  halfnneg2  12494  halfaddsub  12496  nneo  12699  zeo  12701  peano5uzi  12704  fztp  13616  uzrdgxfr  14004  bcn2  14354  bcpasc  14356  hashxplem  14468  hashfun  14472  swrds2  14975  repsw2  14985  repsw3  14986  imre  15143  reim  15144  crim  15150  addcj  15183  imval2  15186  cnpart  15275  01sqrexlem7  15283  absmax  15364  binomfallfaclem2  16072  bpoly2  16089  bpoly3  16090  fsumcube  16092  efgt0  16135  sinf  16156  efi4p  16169  resin4p  16170  recos4p  16171  sinneg  16178  efival  16184  cosadd  16197  sinmul  16204  sinbnd  16212  cosbnd  16213  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  sin01gt0  16222  cos01gt0  16223  sin02gt0  16224  rpnnen2lem11  16256  rpnnen2lem12  16257  odd2np1lem  16373  odd2np1  16374  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem15  16862  pythagtriplem16  16863  pythagtriplem17  16864  pockthi  16940  prmreclem5  16953  prmreclem6  16954  prmlem0  17139  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  isghm  19245  odinf  19595  lbsexg  21183  psgnghm2  21616  mopnex  24547  tngnm  24687  tngngp2  24688  tngngpd  24689  tngngp  24690  addccncf  24956  sub1cncf  24958  sub2cncf  24959  iihalf1  24971  iihalf2  24974  pjthlem1  25484  ovolunlem1a  25544  ovolunlem1  25545  opnmbllem  25649  vitalilem4  25659  iblcnlem1  25837  itgcnlem  25839  dvmptre  26021  dvmptim  26022  dvlipcn  26047  mdegldg  26119  aaliou3lem3  26400  aaliou3lem8  26401  sincosq1lem  26553  sincosq2sgn  26555  sincosq3sgn  26556  sincosq4sgn  26557  sinq12gt0  26563  abssinper  26577  coskpi  26579  sineq0  26580  coseq1  26581  efeq1  26584  resinf1o  26592  efif1olem2  26599  efif1olem4  26601  logneg2  26671  cxpsqrtlem  26758  cxpsqrt  26759  logsqrt  26760  1cubr  26899  leibpilem2  26998  basellem3  27140  ppiub  27262  chtublem  27269  chtub  27270  bcmax  27336  bcp1ctr  27337  bposlem2  27343  bposlem6  27347  bposlem9  27350  logdivsum  27591  elno  27704  mulscl  28174  4ipval2  30736  ipidsq  30738  dipcl  30740  dipcj  30742  ipasslem11  30868  hvmul0  31052  pjhthlem1  31419  h1de2bi  31582  spanunsni  31607  adjeu  31917  nmopge0  31939  nmfnge0  31955  opsqrlem6  32173  mdsl1i  32349  mdsl2bi  32351  mdexchi  32363  superpos  32382  atabsi  32429  dmdbr5ati  32450  cdj3lem1  32462  fpwrelmapffslem  32749  dp2cl  32846  dpfrac1  32858  cshw1s2  32929  ogrpaddlt  33076  ofldlt1  33322  ofldchr  33323  oddpwdc  34335  eulerpartgbij  34353  subfacp1lem2a  35164  subfacp1lem5  35168  subfacp1lem6  35169  subfaclim  35172  sinccvglem  35656  dfon2lem3  35766  dfon2lem7  35770  wsuceq1  35796  clsun  36310  vtoclefex  37316  finxpreclem5  37377  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem22  37628  poimirlem31  37637  opnmbllem0  37642  mblfinlem3  37645  itg2addnclem3  37659  ftc1cnnclem  37677  ftc1anclem6  37684  ftc2nc  37688  dvasin  37690  fdc  37731  constcncf  37748  heiborlem7  37803  atlatmstc  39300  lcmineqlem10  42019  lcmineqlem12  42021  facp2  42124  fac2xp3  42220  sn-00idlem1  42404  0prjspnlem  42609  sn-isghm  42659  diophren  42800  oaabsb  43283  dftrcl3  43709  dfrtrcl3  43722  cotrclrcl  43731  lhe4.4ex1a  44324  dirkerper  46051  zlmodzxznm  48342  sinh-conventional  48969