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:  ceqsex  3468  ceqsexv  3469  moeq3  3642  fvsng  7034  fveqf1o  7155  fliftcnv  7162  fliftfun  7163  cnvct  8778  undom  8800  pwdom  8865  onomeneq  8943  pwfilemOLD  9043  ordiso  9205  ordtypelem8  9214  wdompwdom  9267  unxpwdom  9278  harwdom  9280  inf0  9309  infeq5i  9324  cantnfcl  9355  cardiun  9671  infxpenlem  9700  dfac8b  9718  acnnum  9739  inffien  9750  dfac12lem2  9831  djudoml  9871  cdainflem  9874  djuinf  9875  infunabs  9894  infdju  9895  infdif  9896  infdif2  9897  infmap2  9905  fictb  9932  cofsmo  9956  fin23lem21  10026  hsmexlem1  10113  dmct  10211  mptct  10225  iundomg  10228  iunctb  10261  fpwwe2lem8  10325  canthnum  10336  winalim2  10383  rankcf  10464  tskuni  10470  npomex  10683  hashun2  14026  swrd2lsw  14593  2swrd2eqwrdeq  14594  limsupgord  15109  summolem2  15356  zsum  15358  prodmolem2  15573  zprod  15575  ltoddhalfle  15998  isinv  17389  invsym2  17392  invfun  17393  oppcsect2  17408  oppcinv  17409  efgcpbllemb  19276  frgpuplem  19293  gsumval3  19423  1stcfb  22504  1stcrestlem  22511  2ndcdisj2  22516  txdis1cn  22694  tx1stc  22709  tgphaus  23176  qustgplem  23180  tsmsxp  23214  xmeter  23494  bndth  24027  clmneg1  24151  ovolctb2  24561  ovoliunlem1  24571  i1fd  24750  dvgt0lem2  25072  taylf  25425  efcvx  25513  logccv  25723  loglesqrt  25816  usgredg2v  27497  crctcshtrl  28089  frgr3vlem1  28538  strlem6  30519  mptctf  30954  omsmeas  32190  sibfof  32207  bnj97  32746  bnj553  32778  bnj966  32824  bnj1442  32929  subfaclefac  33038  erdsze2lem1  33065  erdsze2lem2  33066  snmlff  33191  satffunlem2lem2  33268  frxp3  33724  orderseqlem  33728  bj-ssbid2ALT  34771  phpreu  35688  ptrecube  35704  poimirlem3  35707  poimirlem32  35736  heicant  35739  dvhopellsm  39058  pell1qrgaplem  40611  dnwech  40789  mnurndlem1  41788  stoweid  43494  dirkercncflem2  43535  fourierdlem36  43574