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  3525  ceqsexvOLD  3527  moeq3  3709  fvsng  7178  fveqf1o  7301  fliftcnv  7308  fliftfun  7309  frxp3  8137  orderseqlem  8143  cnvct  9034  undomOLD  9060  pwdom  9129  php  9210  onomeneqOLD  9229  pwfilemOLD  9346  ordiso  9511  ordtypelem8  9520  wdompwdom  9573  unxpwdom  9584  harwdom  9586  inf0  9616  infeq5i  9631  cantnfcl  9662  cardiun  9977  infxpenlem  10008  dfac8b  10026  acnnum  10047  inffien  10058  dfac12lem2  10139  djudoml  10179  cdainflem  10182  djuinf  10183  infunabs  10202  infdju  10203  infdif  10204  infdif2  10205  infmap2  10213  fictb  10240  cofsmo  10264  fin23lem21  10334  hsmexlem1  10421  dmct  10519  mptct  10533  iundomg  10536  iunctb  10569  fpwwe2lem8  10633  canthnum  10644  winalim2  10691  rankcf  10772  tskuni  10778  npomex  10991  hashun2  14343  swrd2lsw  14903  2swrd2eqwrdeq  14904  limsupgord  15416  summolem2  15662  zsum  15664  prodmolem2  15879  zprod  15881  ltoddhalfle  16304  isinv  17707  invsym2  17710  invfun  17711  oppcsect2  17726  oppcinv  17727  efgcpbllemb  19623  frgpuplem  19640  gsumval3  19775  1stcfb  22949  1stcrestlem  22956  2ndcdisj2  22961  txdis1cn  23139  tx1stc  23154  tgphaus  23621  qustgplem  23625  tsmsxp  23659  xmeter  23939  bndth  24474  clmneg1  24598  ovolctb2  25009  ovoliunlem1  25019  i1fd  25198  dvgt0lem2  25520  taylf  25873  efcvx  25961  logccv  26171  loglesqrt  26266  0elold  27402  usgredg2v  28484  crctcshtrl  29077  frgr3vlem1  29526  strlem6  31509  mptctf  31942  omsmeas  33322  sibfof  33339  bnj97  33877  bnj553  33909  bnj966  33955  bnj1442  34060  subfaclefac  34167  erdsze2lem1  34194  erdsze2lem2  34195  snmlff  34320  satffunlem2lem2  34397  bj-ssbid2ALT  35540  phpreu  36472  ptrecube  36488  poimirlem3  36491  poimirlem32  36520  heicant  36523  dvhopellsm  39988  pell1qrgaplem  41611  dnwech  41790  oaun3lem1  42124  mnurndlem1  43040  rn1st  43978  stoweid  44779  dirkercncflem2  44820  fourierdlem36  44859