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  3461  moeq3  3617  fvsng  6765  fveqf1o  6883  fliftcnv  6887  fliftfun  6888  cnvct  8383  undom  8401  pwdom  8465  onomeneq  8503  pwfilem  8613  ordiso  8775  ordtypelem8  8784  wdompwdom  8837  unxpwdom  8848  harwdom  8849  infeq5i  8893  cantnfcl  8924  cardiun  9205  infxpenlem  9233  dfac8b  9251  acnnum  9272  inffien  9283  dfac12lem2  9364  djudoml  9408  cdainflem  9411  djuinf  9412  infunabs  9427  infdju  9428  infdif  9429  infdif2  9430  infmap2  9438  fictb  9465  cofsmo  9489  fin23lem21  9559  hsmexlem1  9646  dmct  9744  mptct  9758  iundomg  9761  iunctb  9794  fpwwe2lem9  9858  canthnum  9869  winalim2  9916  rankcf  9997  tskuni  10003  npomex  10216  hashun2  13557  swrd2lsw  14176  2swrd2eqwrdeq  14177  2swrd2eqwrdeqOLD  14178  limsupgord  14690  summolem2  14933  zsum  14935  prodmolem2  15149  zprod  15151  ltoddhalfle  15570  isinv  16888  invsym2  16891  invfun  16892  oppcsect2  16907  oppcinv  16908  efgcpbllemb  18641  frgpuplem  18658  gsumval3  18781  1stcfb  21757  1stcrestlem  21764  2ndcdisj2  21769  txdis1cn  21947  tx1stc  21962  tgphaus  22428  qustgplem  22432  tsmsxp  22466  xmeter  22746  bndth  23265  clmneg1  23389  ovolctb2  23796  ovoliunlem1  23806  i1fd  23985  dvgt0lem2  24303  taylf  24652  efcvx  24740  logccv  24947  loglesqrt  25040  usgredg2v  26712  crctcshtrl  27309  frgr3vlem1  27807  strlem6  29814  mptctf  30212  omsmeas  31232  sibfof  31249  bnj97  31791  bnj553  31823  bnj966  31869  bnj1442  31972  subfaclefac  32014  erdsze2lem1  32041  erdsze2lem2  32042  snmlff  32167  orderseqlem  32621  bj-ssbid2ALT  33511  phpreu  34323  ptrecube  34339  poimirlem3  34342  poimirlem32  34371  heicant  34374  dvhopellsm  37704  pell1qrgaplem  38872  dnwech  39050  mnurndlem1  39998  stoweid  41785  dirkercncflem2  41826  fourierdlem36  41865