Theorem mp3an23 1570

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

Syntax hints:   → wi 4   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  sbciegf  3665  predeq1  5895  wrecseq1  7641  ac6sfi  8439  unfilem1  8459  ordtypelem2  8659  infxpenc2  9124  cda0en  9282  cfsmolem  9373  axdc4lem  9558  1nqenq  10065  mul02lem1  10493  muleqadd  10952  halfcl  11520  rehalfcl  11521  half0  11522  2halves  11523  halfpos2  11524  halfnneg2  11526  halfaddsub  11528  nneo  11723  zeo  11725  peano5uzi  11728  fztp  12616  uzrdgxfr  12986  bcn2  13322  bcpasc  13324  hashxplem  13433  hashfun  13437  swrds2  13905  repsw2  13914  repsw3  13915  imre  14067  reim  14068  crim  14074  addcj  14107  imval2  14110  cnpart  14199  sqrlem7  14208  absmax  14288  binomfallfaclem2  14987  bpoly2  15004  bpoly3  15005  fsumcube  15007  efgt0  15049  sinf  15070  efi4p  15083  resin4p  15084  recos4p  15085  sinneg  15092  efival  15098  cosadd  15111  sinmul  15118  sinbnd  15126  cosbnd  15127  ef01bndlem  15130  sin01bnd  15131  cos01bnd  15132  sin01gt0  15136  cos01gt0  15137  sin02gt0  15138  rpnnen2lem11  15169  rpnnen2lem12  15170  odd2np1lem  15280  odd2np1  15281  pythagtriplem12  15744  pythagtriplem14  15746  pythagtriplem15  15747  pythagtriplem16  15748  pythagtriplem17  15749  pockthi  15824  prmreclem5  15837  prmreclem6  15838  prmlem0  16020  prdsplusg  16319  prdsmulr  16320  prdsvsca  16321  odinf  18177  lbsexg  19369  psgnghm2  20130  mopnex  22534  tngnm  22665  tngngp2  22666  tngngpd  22667  tngngp  22668  addccncf  22929  iihalf1  22940  iihalf2  22942  pjthlem1  23419  ovolunlem1a  23476  ovolunlem1  23477  opnmbllem  23581  vitalilem4  23591  iblcnlem1  23767  itgcnlem  23769  dvmptre  23945  dvmptim  23946  dvlipcn  23970  mdegldg  24039  aaliou3lem3  24312  aaliou3lem8  24313  sincosq1lem  24463  sincosq2sgn  24465  sincosq3sgn  24466  sincosq4sgn  24467  sinq12gt0  24473  abssinper  24484  coskpi  24486  sineq0  24487  coseq1  24488  efeq1  24489  resinf1o  24496  efif1olem2  24503  efif1olem4  24505  logneg2  24574  cxpsqrtlem  24661  cxpsqrt  24662  logsqrt  24663  1cubr  24782  leibpilem1  24880  leibpilem2  24881  basellem3  25022  ppiub  25142  chtublem  25149  chtub  25150  bcmax  25216  bcp1ctr  25217  bposlem2  25223  bposlem6  25227  bposlem9  25230  logdivsum  25435  4ipval2  27890  ipidsq  27892  dipcl  27894  dipcj  27896  ipasslem11  28022  hvmul0  28208  pjhthlem1  28577  h1de2bi  28740  spanunsni  28765  adjeu  29075  nmopge0  29097  nmfnge0  29113  opsqrlem6  29331  mdsl1i  29507  mdsl2bi  29509  mdexchi  29521  superpos  29540  atabsi  29587  dmdbr5ati  29608  cdj3lem1  29620  fpwrelmapffslem  29833  dp2cl  29912  dpfrac1  29924  ogrpaddlt  30042  ofldlt1  30137  ofldchr  30138  oddpwdc  30740  eulerpartgbij  30758  subfacp1lem2a  31483  subfacp1lem5  31487  subfacp1lem6  31488  subfaclim  31491  sinccvglem  31886  dfon2lem3  32008  dfon2lem7  32012  wsuceq1  32079  clsun  32642  vtoclefex  33496  finxpreclem5  33546  sin2h  33710  cos2h  33711  tan2h  33712  poimirlem22  33742  poimirlem31  33751  opnmbllem0  33756  mblfinlem3  33759  itg2addnclem3  33773  ftc1cnnclem  33793  ftc1anclem6  33800  ftc2nc  33804  dvasin  33806  fdc  33850  constcncf  33867  sub1cncf  33869  sub2cncf  33870  heiborlem7  33925  atlatmstc  35097  diophren  37876  dftrcl3  38509  dfrtrcl3  38522  cotrclrcl  38531  lhe4.4ex1a  39025  dirkerper  40789  zlmodzxznm  42851  sinh-conventional  43048