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  3660  fvsng  7131  fveqf1o  7253  fliftcnv  7262  fliftfun  7263  frxp3  8098  orderseqlem  8104  cnvct  8978  pwdom  9064  php  9138  ordiso  9428  ordtypelem8  9437  wdompwdom  9490  unxpwdom  9501  harwdom  9503  inf0  9540  infeq5i  9555  cantnfcl  9586  cardiun  9904  infxpenlem  9933  dfac8b  9951  acnnum  9972  inffien  9983  dfac12lem2  10065  djudoml  10105  cdainflem  10108  djuinf  10109  infunabs  10126  infdju  10127  infdif  10128  infdif2  10129  infmap2  10137  fictb  10164  cofsmo  10189  fin23lem21  10259  hsmexlem1  10346  dmct  10444  mptct  10458  iundomg  10461  iunctb  10495  fpwwe2lem8  10559  canthnum  10570  winalim2  10617  rankcf  10698  tskuni  10704  npomex  10917  hashun2  14343  swrd2lsw  14912  2swrd2eqwrdeq  14913  limsupgord  15432  summolem2  15676  zsum  15678  prodmolem2  15898  zprod  15900  ltoddhalfle  16328  isinv  17725  invsym2  17728  invfun  17729  oppcsect2  17744  oppcinv  17745  efgcpbllemb  19728  frgpuplem  19745  gsumval3  19880  1stcfb  23435  1stcrestlem  23442  2ndcdisj2  23447  txdis1cn  23625  tx1stc  23640  tgphaus  24107  qustgplem  24111  tsmsxp  24145  xmeter  24423  bndth  24950  clmneg1  25074  ovolctb2  25484  ovoliunlem1  25494  i1fd  25673  dvgt0lem2  25995  taylf  26351  efcvx  26439  logccv  26652  loglesqrt  26750  0elold  27927  noseqrdgfn  28323  n0fincut  28372  usgredg2v  29321  crctcshtrl  29916  frgr3vlem1  30368  strlem6  32352  mptctf  32815  omsmeas  34514  sibfof  34531  bnj97  35055  bnj553  35087  bnj966  35133  bnj1442  35238  tz9.1regs  35322  subfaclefac  35411  erdsze2lem1  35438  erdsze2lem2  35439  snmlff  35564  satffunlem2lem2  35641  bj-ssbid2ALT  37010  phpreu  37978  ptrecube  37994  poimirlem3  37997  poimirlem32  38026  heicant  38029  dvhopellsm  41616  aks5lem7  42692  pell1qrgaplem  43325  dnwech  43500  oaun3lem1  43826  mnurndlem1  44732  rn1st  45724  stoweid  46513  dirkercncflem2  46554  fourierdlem36  46593  usgrexmpl12ngric  48536  usgrexmpl12ngrlic  48537