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:  moeq3  3667  fvsng  7120  fveqf1o  7242  fliftcnv  7251  fliftfun  7252  frxp3  8087  orderseqlem  8093  cnvct  8963  pwdom  9049  php  9123  ordiso  9409  ordtypelem8  9418  wdompwdom  9471  unxpwdom  9482  harwdom  9484  inf0  9518  infeq5i  9533  cantnfcl  9564  cardiun  9882  infxpenlem  9911  dfac8b  9929  acnnum  9950  inffien  9961  dfac12lem2  10043  djudoml  10083  cdainflem  10086  djuinf  10087  infunabs  10104  infdju  10105  infdif  10106  infdif2  10107  infmap2  10115  fictb  10142  cofsmo  10167  fin23lem21  10237  hsmexlem1  10324  dmct  10422  mptct  10436  iundomg  10439  iunctb  10472  fpwwe2lem8  10536  canthnum  10547  winalim2  10594  rankcf  10675  tskuni  10681  npomex  10894  hashun2  14292  swrd2lsw  14861  2swrd2eqwrdeq  14862  limsupgord  15381  summolem2  15625  zsum  15627  prodmolem2  15844  zprod  15846  ltoddhalfle  16274  isinv  17669  invsym2  17672  invfun  17673  oppcsect2  17688  oppcinv  17689  efgcpbllemb  19669  frgpuplem  19686  gsumval3  19821  1stcfb  23361  1stcrestlem  23368  2ndcdisj2  23373  txdis1cn  23551  tx1stc  23566  tgphaus  24033  qustgplem  24037  tsmsxp  24071  xmeter  24349  bndth  24885  clmneg1  25010  ovolctb2  25421  ovoliunlem1  25431  i1fd  25610  dvgt0lem2  25936  taylf  26296  efcvx  26387  logccv  26600  loglesqrt  26699  0elold  27856  noseqrdgfn  28237  n0sfincut  28283  usgredg2v  29207  crctcshtrl  29803  frgr3vlem1  30255  strlem6  32238  mptctf  32703  omsmeas  34357  sibfof  34374  bnj97  34899  bnj553  34931  bnj966  34977  bnj1442  35082  tz9.1regs  35151  subfaclefac  35241  erdsze2lem1  35268  erdsze2lem2  35269  snmlff  35394  satffunlem2lem2  35471  bj-ssbid2ALT  36728  phpreu  37664  ptrecube  37680  poimirlem3  37683  poimirlem32  37712  heicant  37715  dvhopellsm  41236  aks5lem7  42313  pell1qrgaplem  42990  dnwech  43165  oaun3lem1  43491  mnurndlem1  44398  rn1st  45394  stoweid  46185  dirkercncflem2  46226  fourierdlem36  46265  usgrexmpl12ngric  48162  usgrexmpl12ngrlic  48163