Theorem mpisyl 21

Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.)

Hypotheses

Ref	Expression
mpisyl.1	⊢ (𝜑 → 𝜓)
mpisyl.2	⊢ 𝜒
mpisyl.3	⊢ (𝜓 → (𝜒 → 𝜃))

Assertion

Ref	Expression
mpisyl	⊢ (𝜑 → 𝜃)

Proof of Theorem mpisyl

Step	Hyp	Ref	Expression
1		mpisyl.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpisyl.2	. . 3 ⊢ 𝜒
3		mpisyl.3	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
4	2, 3	mpi 20	. 2 ⊢ (𝜓 → 𝜃)
5	1, 4	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  moeq3  3672  fvsng  7136  fveqf1o  7258  fliftcnv  7267  fliftfun  7268  frxp3  8103  orderseqlem  8109  cnvct  8983  pwdom  9069  php  9143  ordiso  9433  ordtypelem8  9442  wdompwdom  9495  unxpwdom  9506  harwdom  9508  inf0  9542  infeq5i  9557  cantnfcl  9588  cardiun  9906  infxpenlem  9935  dfac8b  9953  acnnum  9974  inffien  9985  dfac12lem2  10067  djudoml  10107  cdainflem  10110  djuinf  10111  infunabs  10128  infdju  10129  infdif  10130  infdif2  10131  infmap2  10139  fictb  10166  cofsmo  10191  fin23lem21  10261  hsmexlem1  10348  dmct  10446  mptct  10460  iundomg  10463  iunctb  10497  fpwwe2lem8  10561  canthnum  10572  winalim2  10619  rankcf  10700  tskuni  10706  npomex  10919  hashun2  14318  swrd2lsw  14887  2swrd2eqwrdeq  14888  limsupgord  15407  summolem2  15651  zsum  15653  prodmolem2  15870  zprod  15872  ltoddhalfle  16300  isinv  17696  invsym2  17699  invfun  17700  oppcsect2  17715  oppcinv  17716  efgcpbllemb  19696  frgpuplem  19713  gsumval3  19848  1stcfb  23401  1stcrestlem  23408  2ndcdisj2  23413  txdis1cn  23591  tx1stc  23606  tgphaus  24073  qustgplem  24077  tsmsxp  24111  xmeter  24389  bndth  24925  clmneg1  25050  ovolctb2  25461  ovoliunlem1  25471  i1fd  25650  dvgt0lem2  25976  taylf  26336  efcvx  26427  logccv  26640  loglesqrt  26739  0elold  27918  noseqrdgfn  28314  n0fincut  28363  usgredg2v  29312  crctcshtrl  29908  frgr3vlem1  30360  strlem6  32343  mptctf  32805  omsmeas  34500  sibfof  34517  bnj97  35041  bnj553  35073  bnj966  35119  bnj1442  35224  tz9.1regs  35309  subfaclefac  35389  erdsze2lem1  35416  erdsze2lem2  35417  snmlff  35542  satffunlem2lem2  35619  bj-ssbid2ALT  36902  phpreu  37849  ptrecube  37865  poimirlem3  37868  poimirlem32  37897  heicant  37900  dvhopellsm  41487  aks5lem7  42564  pell1qrgaplem  43224  dnwech  43399  oaun3lem1  43725  mnurndlem1  44631  rn1st  45625  stoweid  46415  dirkercncflem2  46456  fourierdlem36  46495  usgrexmpl12ngric  48392  usgrexmpl12ngrlic  48393