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  3491  ceqsexvOLD  3493  moeq3  3668  fvsng  7122  fveqf1o  7245  fliftcnv  7252  fliftfun  7253  frxp3  8075  orderseqlem  8081  cnvct  8936  undomOLD  8962  pwdom  9031  php  9112  onomeneqOLD  9131  pwfilemOLD  9248  ordiso  9410  ordtypelem8  9419  wdompwdom  9472  unxpwdom  9483  harwdom  9485  inf0  9515  infeq5i  9530  cantnfcl  9561  cardiun  9876  infxpenlem  9907  dfac8b  9925  acnnum  9946  inffien  9957  dfac12lem2  10038  djudoml  10078  cdainflem  10081  djuinf  10082  infunabs  10101  infdju  10102  infdif  10103  infdif2  10104  infmap2  10112  fictb  10139  cofsmo  10163  fin23lem21  10233  hsmexlem1  10320  dmct  10418  mptct  10432  iundomg  10435  iunctb  10468  fpwwe2lem8  10532  canthnum  10543  winalim2  10590  rankcf  10671  tskuni  10677  npomex  10890  hashun2  14237  swrd2lsw  14795  2swrd2eqwrdeq  14796  limsupgord  15308  summolem2  15555  zsum  15557  prodmolem2  15772  zprod  15774  ltoddhalfle  16197  isinv  17597  invsym2  17600  invfun  17601  oppcsect2  17616  oppcinv  17617  efgcpbllemb  19490  frgpuplem  19507  gsumval3  19637  1stcfb  22742  1stcrestlem  22749  2ndcdisj2  22754  txdis1cn  22932  tx1stc  22947  tgphaus  23414  qustgplem  23418  tsmsxp  23452  xmeter  23732  bndth  24267  clmneg1  24391  ovolctb2  24802  ovoliunlem1  24812  i1fd  24991  dvgt0lem2  25313  taylf  25666  efcvx  25754  logccv  25964  loglesqrt  26057  usgredg2v  28020  crctcshtrl  28613  frgr3vlem1  29062  strlem6  31043  mptctf  31476  omsmeas  32751  sibfof  32768  bnj97  33306  bnj553  33338  bnj966  33384  bnj1442  33489  subfaclefac  33598  erdsze2lem1  33625  erdsze2lem2  33626  snmlff  33751  satffunlem2lem2  33828  bj-ssbid2ALT  35059  phpreu  35994  ptrecube  36010  poimirlem3  36013  poimirlem32  36042  heicant  36045  dvhopellsm  39512  pell1qrgaplem  41099  dnwech  41278  mnurndlem1  42466  rn1st  43402  stoweid  44199  dirkercncflem2  44240  fourierdlem36  44279