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  3659  fvsng  7128  fveqf1o  7250  fliftcnv  7259  fliftfun  7260  frxp3  8094  orderseqlem  8100  cnvct  8974  pwdom  9060  php  9134  ordiso  9424  ordtypelem8  9433  wdompwdom  9486  unxpwdom  9497  harwdom  9499  inf0  9533  infeq5i  9548  cantnfcl  9579  cardiun  9897  infxpenlem  9926  dfac8b  9944  acnnum  9965  inffien  9976  dfac12lem2  10058  djudoml  10098  cdainflem  10101  djuinf  10102  infunabs  10119  infdju  10120  infdif  10121  infdif2  10122  infmap2  10130  fictb  10157  cofsmo  10182  fin23lem21  10252  hsmexlem1  10339  dmct  10437  mptct  10451  iundomg  10454  iunctb  10488  fpwwe2lem8  10552  canthnum  10563  winalim2  10610  rankcf  10691  tskuni  10697  npomex  10910  hashun2  14336  swrd2lsw  14905  2swrd2eqwrdeq  14906  limsupgord  15425  summolem2  15669  zsum  15671  prodmolem2  15891  zprod  15893  ltoddhalfle  16321  isinv  17718  invsym2  17721  invfun  17722  oppcsect2  17737  oppcinv  17738  efgcpbllemb  19721  frgpuplem  19738  gsumval3  19873  1stcfb  23420  1stcrestlem  23427  2ndcdisj2  23432  txdis1cn  23610  tx1stc  23625  tgphaus  24092  qustgplem  24096  tsmsxp  24130  xmeter  24408  bndth  24935  clmneg1  25059  ovolctb2  25469  ovoliunlem1  25479  i1fd  25658  dvgt0lem2  25980  taylf  26337  efcvx  26427  logccv  26640  loglesqrt  26738  0elold  27916  noseqrdgfn  28312  n0fincut  28361  usgredg2v  29310  crctcshtrl  29906  frgr3vlem1  30358  strlem6  32342  mptctf  32804  omsmeas  34483  sibfof  34500  bnj97  35024  bnj553  35056  bnj966  35102  bnj1442  35207  tz9.1regs  35294  subfaclefac  35374  erdsze2lem1  35401  erdsze2lem2  35402  snmlff  35527  satffunlem2lem2  35604  bj-ssbid2ALT  36973  phpreu  37939  ptrecube  37955  poimirlem3  37958  poimirlem32  37987  heicant  37990  dvhopellsm  41577  aks5lem7  42653  pell1qrgaplem  43319  dnwech  43494  oaun3lem1  43820  mnurndlem1  44726  rn1st  45720  stoweid  46509  dirkercncflem2  46550  fourierdlem36  46589  usgrexmpl12ngric  48526  usgrexmpl12ngrlic  48527