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  3510  moeq3  3695  fvsng  7171  fveqf1o  7294  fliftcnv  7303  fliftfun  7304  frxp3  8148  orderseqlem  8154  cnvct  9046  undomOLD  9072  pwdom  9141  php  9219  onomeneqOLD  9236  ordiso  9528  ordtypelem8  9537  wdompwdom  9590  unxpwdom  9601  harwdom  9603  inf0  9633  infeq5i  9648  cantnfcl  9679  cardiun  9994  infxpenlem  10025  dfac8b  10043  acnnum  10064  inffien  10075  dfac12lem2  10157  djudoml  10197  cdainflem  10200  djuinf  10201  infunabs  10218  infdju  10219  infdif  10220  infdif2  10221  infmap2  10229  fictb  10256  cofsmo  10281  fin23lem21  10351  hsmexlem1  10438  dmct  10536  mptct  10550  iundomg  10553  iunctb  10586  fpwwe2lem8  10650  canthnum  10661  winalim2  10708  rankcf  10789  tskuni  10795  npomex  11008  hashun2  14399  swrd2lsw  14969  2swrd2eqwrdeq  14970  limsupgord  15486  summolem2  15730  zsum  15732  prodmolem2  15949  zprod  15951  ltoddhalfle  16378  isinv  17771  invsym2  17774  invfun  17775  oppcsect2  17790  oppcinv  17791  efgcpbllemb  19734  frgpuplem  19751  gsumval3  19886  1stcfb  23381  1stcrestlem  23388  2ndcdisj2  23393  txdis1cn  23571  tx1stc  23586  tgphaus  24053  qustgplem  24057  tsmsxp  24091  xmeter  24370  bndth  24906  clmneg1  25031  ovolctb2  25443  ovoliunlem1  25453  i1fd  25632  dvgt0lem2  25958  taylf  26318  efcvx  26409  logccv  26622  loglesqrt  26721  0elold  27864  noseqrdgfn  28229  usgredg2v  29152  crctcshtrl  29751  frgr3vlem1  30200  strlem6  32183  mptctf  32641  omsmeas  34301  sibfof  34318  bnj97  34843  bnj553  34875  bnj966  34921  bnj1442  35026  subfaclefac  35144  erdsze2lem1  35171  erdsze2lem2  35172  snmlff  35297  satffunlem2lem2  35374  bj-ssbid2ALT  36627  phpreu  37574  ptrecube  37590  poimirlem3  37593  poimirlem32  37622  heicant  37625  dvhopellsm  41082  aks5lem7  42159  pell1qrgaplem  42843  dnwech  43019  oaun3lem1  43345  mnurndlem1  44253  rn1st  45245  stoweid  46040  dirkercncflem2  46081  fourierdlem36  46120  usgrexmpl12ngric  47990  usgrexmpl12ngrlic  47991