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  3497  moeq3  3683  fvsng  7154  fveqf1o  7277  fliftcnv  7286  fliftfun  7287  frxp3  8130  orderseqlem  8136  cnvct  9005  pwdom  9093  php  9171  ordiso  9469  ordtypelem8  9478  wdompwdom  9531  unxpwdom  9542  harwdom  9544  inf0  9574  infeq5i  9589  cantnfcl  9620  cardiun  9935  infxpenlem  9966  dfac8b  9984  acnnum  10005  inffien  10016  dfac12lem2  10098  djudoml  10138  cdainflem  10141  djuinf  10142  infunabs  10159  infdju  10160  infdif  10161  infdif2  10162  infmap2  10170  fictb  10197  cofsmo  10222  fin23lem21  10292  hsmexlem1  10379  dmct  10477  mptct  10491  iundomg  10494  iunctb  10527  fpwwe2lem8  10591  canthnum  10602  winalim2  10649  rankcf  10730  tskuni  10736  npomex  10949  hashun2  14348  swrd2lsw  14918  2swrd2eqwrdeq  14919  limsupgord  15438  summolem2  15682  zsum  15684  prodmolem2  15901  zprod  15903  ltoddhalfle  16331  isinv  17722  invsym2  17725  invfun  17726  oppcsect2  17741  oppcinv  17742  efgcpbllemb  19685  frgpuplem  19702  gsumval3  19837  1stcfb  23332  1stcrestlem  23339  2ndcdisj2  23344  txdis1cn  23522  tx1stc  23537  tgphaus  24004  qustgplem  24008  tsmsxp  24042  xmeter  24321  bndth  24857  clmneg1  24982  ovolctb2  25393  ovoliunlem1  25403  i1fd  25582  dvgt0lem2  25908  taylf  26268  efcvx  26359  logccv  26572  loglesqrt  26671  0elold  27821  noseqrdgfn  28200  n0sfincut  28246  usgredg2v  29154  crctcshtrl  29753  frgr3vlem1  30202  strlem6  32185  mptctf  32641  omsmeas  34314  sibfof  34331  bnj97  34856  bnj553  34888  bnj966  34934  bnj1442  35039  subfaclefac  35163  erdsze2lem1  35190  erdsze2lem2  35191  snmlff  35316  satffunlem2lem2  35393  bj-ssbid2ALT  36651  phpreu  37598  ptrecube  37614  poimirlem3  37617  poimirlem32  37646  heicant  37649  dvhopellsm  41111  aks5lem7  42188  pell1qrgaplem  42861  dnwech  43037  oaun3lem1  43363  mnurndlem1  44270  rn1st  45267  stoweid  46061  dirkercncflem2  46102  fourierdlem36  46141  usgrexmpl12ngric  48029  usgrexmpl12ngrlic  48030