Theorem sylancr 393

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancr.1	⊢ ψ
sylancr.2	⊢ (φ → χ)
sylancr.3	⊢ ((ψ ∧ χ) → θ)

Assertion

Ref	Expression
sylancr	⊢ (φ → θ)

Proof of Theorem sylancr

Step	Hyp	Ref	Expression
1		sylancr.1	. . 3 ⊢ ψ
2	1	a1i 9	. 2 ⊢ (φ → ψ)
3		sylancr.2	. 2 ⊢ (φ → χ)
4		sylancr.3	. 2 ⊢ ((ψ ∧ χ) → θ)
5	2, 3, 4	syl2anc 391	1 ⊢ (φ → θ)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101

This theorem is referenced by:  mpteq2da  3837  unipw  3944  opeluu  4148  uniexb  4171  unon  4202  opeliunxp  4338  xpexg  4395  resiexg  4596  imaexg  4623  exse2  4642  soirri  4662  djudisj  4693  elxp5  4752  cnvexg  4798  cnviinm  4802  coexg  4805  funssres  4885  f1oabexg  5081  sefvex  5139  ssimaex  5177  mptfvex  5199  f1ompt  5263  fmptcof  5274  resfunexg  5325  mptexg  5329  funfvima3  5335  ovid  5559  ov  5562  ofres  5667  cofunexg  5680  opabex3d  5690  opabex3  5691  oprabexd  5696  1stcof  5732  2ndcof  5733  mpt2exxg  5775  cnvf1o  5788  f2ndf  5789  tposexg  5814  tfrlemisucaccv  5880  tfrlemibxssdm  5882  tfrlemibfn  5883  tfrlemi14d  5888  rdgtfr  5901  rdgruledefgg  5902  frecabex  5923  omcl  5980  erth  6086  th3qlem1  6144  fundmen  6222  snfig  6227  unen  6229  xpdom2  6241  nnnq0lem1  6428  addnqpr1lemil  6539  addnqpr1lemiu  6540  prsrlem1  6630  gt0srpr  6636  mulcnsr  6692  mulcnsrec  6700  axmulass  6717  axdistr  6718  mulid1  6782  axmulgt0  6848  cnegexlem2  6944  cnegex  6946  gt0ne0d  7259  recexre  7322  msqge0  7360  mulge0  7363  recgt0  7557  recreclt  7607  cju  7654  nnge1  7678  nnnlt1  7681  nn0nlt0  7944  elz2  8048  nnm1ge0  8062  recnz  8069  zneo  8075  uz3m2nn  8251  eluz2b2  8276  nn01to3  8288  mnflt  8434  lincmb01cmp  8601  iccf1o  8602  fz1n  8638  fseq1p1m1  8686  fznn0  8704  fzctr  8721  4fvwrd4  8727  elfzonlteqm1  8796  frec2uzf1od  8833  frecuzrdgrom  8837  frecfzennn  8844  frecfzen2  8845  fzfig  8847  expgt1  8907  expubnd  8925  binom2sub  8977  binom3  8979  zesq  8980  bernneq  8982  bernneq2  8983  expnbnd  8985  expnlbnd2  8987  crre  9045  crim  9046  remim  9048  mulreap  9052  cjreb  9054  recj  9055  reneg  9056  readd  9057  remullem  9059  imcj  9063  imneg  9064  imadd  9065  cjadd  9072  cjneg  9078  imval2  9082  cjreim  9091  cnrecnv  9098