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:  ceqsex  3540  moeq3  3703  fvsng  6942  fveqf1o  7058  fliftcnv  7064  fliftfun  7065  cnvct  8586  undom  8605  pwdom  8669  onomeneq  8708  pwfilem  8818  ordiso  8980  ordtypelem8  8989  wdompwdom  9042  unxpwdom  9053  harwdom  9054  infeq5i  9099  cantnfcl  9130  cardiun  9411  infxpenlem  9439  dfac8b  9457  acnnum  9478  inffien  9489  dfac12lem2  9570  djudoml  9610  cdainflem  9613  djuinf  9614  infunabs  9629  infdju  9630  infdif  9631  infdif2  9632  infmap2  9640  fictb  9667  cofsmo  9691  fin23lem21  9761  hsmexlem1  9848  dmct  9946  mptct  9960  iundomg  9963  iunctb  9996  fpwwe2lem9  10060  canthnum  10071  winalim2  10118  rankcf  10199  tskuni  10205  npomex  10418  hashun2  13745  swrd2lsw  14314  2swrd2eqwrdeq  14315  limsupgord  14829  summolem2  15073  zsum  15075  prodmolem2  15289  zprod  15291  ltoddhalfle  15710  isinv  17030  invsym2  17033  invfun  17034  oppcsect2  17049  oppcinv  17050  efgcpbllemb  18881  frgpuplem  18898  gsumval3  19027  1stcfb  22053  1stcrestlem  22060  2ndcdisj2  22065  txdis1cn  22243  tx1stc  22258  tgphaus  22725  qustgplem  22729  tsmsxp  22763  xmeter  23043  bndth  23562  clmneg1  23686  ovolctb2  24093  ovoliunlem1  24103  i1fd  24282  dvgt0lem2  24600  taylf  24949  efcvx  25037  logccv  25246  loglesqrt  25339  usgredg2v  27009  crctcshtrl  27601  frgr3vlem1  28052  strlem6  30033  mptctf  30453  omsmeas  31581  sibfof  31598  bnj97  32138  bnj553  32170  bnj966  32216  bnj1442  32321  subfaclefac  32423  erdsze2lem1  32450  erdsze2lem2  32451  snmlff  32576  satffunlem2lem2  32653  orderseqlem  33094  bj-ssbid2ALT  33996  phpreu  34891  ptrecube  34907  poimirlem3  34910  poimirlem32  34939  heicant  34942  dvhopellsm  38268  pell1qrgaplem  39490  dnwech  39668  mnurndlem1  40637  stoweid  42368  dirkercncflem2  42409  fourierdlem36  42448