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  ltnnnq  6406  nnnq0lem1  6429  addnqprlemfl  6540  addnqprlemfu  6541  prsrlem1  6670  gt0srpr  6676  mulcnsr  6732  mulcnsrec  6740  axmulass  6757  axdistr  6758  mulid1  6822  axmulgt0  6888  cnegexlem2  6984  cnegex  6986  gt0ne0d  7299  recexre  7362  msqge0  7400  mulge0  7403  recgt0  7597  recreclt  7647  cju  7694  nnge1  7718  nnnlt1  7721  nn0nlt0  7984  elz2  8088  nnm1ge0  8102  recnz  8109  zneo  8115  uz3m2nn  8291  eluz2b2  8316  nn01to3  8328  mnflt  8474  lincmb01cmp  8641  iccf1o  8642  fz1n  8678  fseq1p1m1  8726  fznn0  8744  fzctr  8761  4fvwrd4  8767  elfzonlteqm1  8836  frec2uzf1od  8873  frecuzrdgrom  8877  frecfzennn  8884  frecfzen2  8885  fzfig  8887  expgt1  8947  expubnd  8965  binom2sub  9017  binom3  9019  zesq  9020  bernneq  9022  bernneq2  9023  expnbnd  9025  expnlbnd2  9027  crre  9085  crim  9086  remim  9088  mulreap  9092  cjreb  9094  recj  9095  reneg  9096  readd  9097  remullem  9099  imcj  9103  imneg  9104  imadd  9105  cjadd  9112  cjneg  9118  imval2  9122  cjreim  9131  cnrecnv  9138  absval  9210  rennim  9211