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:  ceqsexOLD  3524  ceqsexvOLD  3526  moeq3  3708  fvsng  7180  fveqf1o  7303  fliftcnv  7310  fliftfun  7311  frxp3  8139  orderseqlem  8145  cnvct  9036  undomOLD  9062  pwdom  9131  php  9212  onomeneqOLD  9231  pwfilemOLD  9348  ordiso  9513  ordtypelem8  9522  wdompwdom  9575  unxpwdom  9586  harwdom  9588  inf0  9618  infeq5i  9633  cantnfcl  9664  cardiun  9979  infxpenlem  10010  dfac8b  10028  acnnum  10049  inffien  10060  dfac12lem2  10141  djudoml  10181  cdainflem  10184  djuinf  10185  infunabs  10204  infdju  10205  infdif  10206  infdif2  10207  infmap2  10215  fictb  10242  cofsmo  10266  fin23lem21  10336  hsmexlem1  10423  dmct  10521  mptct  10535  iundomg  10538  iunctb  10571  fpwwe2lem8  10635  canthnum  10646  winalim2  10693  rankcf  10774  tskuni  10780  npomex  10993  hashun2  14347  swrd2lsw  14907  2swrd2eqwrdeq  14908  limsupgord  15420  summolem2  15666  zsum  15668  prodmolem2  15883  zprod  15885  ltoddhalfle  16308  isinv  17711  invsym2  17714  invfun  17715  oppcsect2  17730  oppcinv  17731  efgcpbllemb  19664  frgpuplem  19681  gsumval3  19816  1stcfb  23169  1stcrestlem  23176  2ndcdisj2  23181  txdis1cn  23359  tx1stc  23374  tgphaus  23841  qustgplem  23845  tsmsxp  23879  xmeter  24159  bndth  24698  clmneg1  24822  ovolctb2  25233  ovoliunlem1  25243  i1fd  25422  dvgt0lem2  25744  taylf  26097  efcvx  26185  logccv  26395  loglesqrt  26490  0elold  27628  usgredg2v  28739  crctcshtrl  29332  frgr3vlem1  29781  strlem6  31764  mptctf  32197  omsmeas  33608  sibfof  33625  bnj97  34163  bnj553  34195  bnj966  34241  bnj1442  34346  subfaclefac  34453  erdsze2lem1  34480  erdsze2lem2  34481  snmlff  34606  satffunlem2lem2  34683  bj-ssbid2ALT  35843  phpreu  36775  ptrecube  36791  poimirlem3  36794  poimirlem32  36823  heicant  36826  dvhopellsm  40291  pell1qrgaplem  41913  dnwech  42092  oaun3lem1  42426  mnurndlem1  43342  rn1st  44277  stoweid  45078  dirkercncflem2  45119  fourierdlem36  45158