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  3488  moeq3  3674  fvsng  7120  fveqf1o  7243  fliftcnv  7252  fliftfun  7253  frxp3  8091  orderseqlem  8097  cnvct  8966  pwdom  9053  php  9131  ordiso  9427  ordtypelem8  9436  wdompwdom  9489  unxpwdom  9500  harwdom  9502  inf0  9536  infeq5i  9551  cantnfcl  9582  cardiun  9897  infxpenlem  9926  dfac8b  9944  acnnum  9965  inffien  9976  dfac12lem2  10058  djudoml  10098  cdainflem  10101  djuinf  10102  infunabs  10119  infdju  10120  infdif  10121  infdif2  10122  infmap2  10130  fictb  10157  cofsmo  10182  fin23lem21  10252  hsmexlem1  10339  dmct  10437  mptct  10451  iundomg  10454  iunctb  10487  fpwwe2lem8  10551  canthnum  10562  winalim2  10609  rankcf  10690  tskuni  10696  npomex  10909  hashun2  14308  swrd2lsw  14877  2swrd2eqwrdeq  14878  limsupgord  15397  summolem2  15641  zsum  15643  prodmolem2  15860  zprod  15862  ltoddhalfle  16290  isinv  17685  invsym2  17688  invfun  17689  oppcsect2  17704  oppcinv  17705  efgcpbllemb  19652  frgpuplem  19669  gsumval3  19804  1stcfb  23348  1stcrestlem  23355  2ndcdisj2  23360  txdis1cn  23538  tx1stc  23553  tgphaus  24020  qustgplem  24024  tsmsxp  24058  xmeter  24337  bndth  24873  clmneg1  24998  ovolctb2  25409  ovoliunlem1  25419  i1fd  25598  dvgt0lem2  25924  taylf  26284  efcvx  26375  logccv  26588  loglesqrt  26687  0elold  27842  noseqrdgfn  28223  n0sfincut  28269  usgredg2v  29190  crctcshtrl  29786  frgr3vlem1  30235  strlem6  32218  mptctf  32674  omsmeas  34290  sibfof  34307  bnj97  34832  bnj553  34864  bnj966  34910  bnj1442  35015  tz9.1regs  35066  subfaclefac  35148  erdsze2lem1  35175  erdsze2lem2  35176  snmlff  35301  satffunlem2lem2  35378  bj-ssbid2ALT  36636  phpreu  37583  ptrecube  37599  poimirlem3  37602  poimirlem32  37631  heicant  37634  dvhopellsm  41096  aks5lem7  42173  pell1qrgaplem  42846  dnwech  43021  oaun3lem1  43347  mnurndlem1  44254  rn1st  45251  stoweid  46045  dirkercncflem2  46086  fourierdlem36  46125  usgrexmpl12ngric  48023  usgrexmpl12ngrlic  48024