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  3513  ceqsexvOLD  3515  moeq3  3704  fvsng  7189  fveqf1o  7311  fliftcnv  7318  fliftfun  7319  frxp3  8156  orderseqlem  8162  cnvct  9059  undomOLD  9085  pwdom  9154  php  9235  onomeneqOLD  9254  pwfilemOLD  9372  ordiso  9541  ordtypelem8  9550  wdompwdom  9603  unxpwdom  9614  harwdom  9616  inf0  9646  infeq5i  9661  cantnfcl  9692  cardiun  10007  infxpenlem  10038  dfac8b  10056  acnnum  10077  inffien  10088  dfac12lem2  10169  djudoml  10209  cdainflem  10212  djuinf  10213  infunabs  10232  infdju  10233  infdif  10234  infdif2  10235  infmap2  10243  fictb  10270  cofsmo  10294  fin23lem21  10364  hsmexlem1  10451  dmct  10549  mptct  10563  iundomg  10566  iunctb  10599  fpwwe2lem8  10663  canthnum  10674  winalim2  10721  rankcf  10802  tskuni  10808  npomex  11021  hashun2  14378  swrd2lsw  14939  2swrd2eqwrdeq  14940  limsupgord  15452  summolem2  15698  zsum  15700  prodmolem2  15915  zprod  15917  ltoddhalfle  16341  isinv  17746  invsym2  17749  invfun  17750  oppcsect2  17765  oppcinv  17766  efgcpbllemb  19722  frgpuplem  19739  gsumval3  19874  1stcfb  23393  1stcrestlem  23400  2ndcdisj2  23405  txdis1cn  23583  tx1stc  23598  tgphaus  24065  qustgplem  24069  tsmsxp  24103  xmeter  24383  bndth  24928  clmneg1  25053  ovolctb2  25465  ovoliunlem1  25475  i1fd  25654  dvgt0lem2  25980  taylf  26340  efcvx  26431  logccv  26642  loglesqrt  26738  0elold  27881  noseqrdgfn  28229  usgredg2v  29112  crctcshtrl  29706  frgr3vlem1  30155  strlem6  32138  mptctf  32581  omsmeas  34074  sibfof  34091  bnj97  34628  bnj553  34660  bnj966  34706  bnj1442  34811  subfaclefac  34917  erdsze2lem1  34944  erdsze2lem2  34945  snmlff  35070  satffunlem2lem2  35147  bj-ssbid2ALT  36270  phpreu  37208  ptrecube  37224  poimirlem3  37227  poimirlem32  37256  heicant  37259  dvhopellsm  40720  pell1qrgaplem  42435  dnwech  42614  oaun3lem1  42945  mnurndlem1  43860  rn1st  44788  stoweid  45589  dirkercncflem2  45630  fourierdlem36  45669