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  addnqprlemfl  6539  addnqprlemfu  6540  prsrlem1  6650  gt0srpr  6656  mulcnsr  6712  mulcnsrec  6720  axmulass  6737  axdistr  6738  mulid1  6802  axmulgt0  6868  cnegexlem2  6964  cnegex  6966  gt0ne0d  7279  recexre  7342  msqge0  7380  mulge0  7383  recgt0  7577  recreclt  7627  cju  7674  nnge1  7698  nnnlt1  7701  nn0nlt0  7964  elz2  8068  nnm1ge0  8082  recnz  8089  zneo  8095  uz3m2nn  8271  eluz2b2  8296  nn01to3  8308  mnflt  8454  lincmb01cmp  8621  iccf1o  8622  fz1n  8658  fseq1p1m1  8706  fznn0  8724  fzctr  8741  4fvwrd4  8747  elfzonlteqm1  8816  frec2uzf1od  8853  frecuzrdgrom  8857  frecfzennn  8864  frecfzen2  8865  fzfig  8867  expgt1  8927  expubnd  8945  binom2sub  8997  binom3  8999  zesq  9000  bernneq  9002  bernneq2  9003  expnbnd  9005  expnlbnd2  9007  crre  9065  crim  9066  remim  9068  mulreap  9072  cjreb  9074  recj  9075  reneg  9076  readd  9077  remullem  9079  imcj  9083  imneg  9084  imadd  9085  cjadd  9092  cjneg  9098  imval2  9102  cjreim  9111  cnrecnv  9118  absval  9190  rennim  9191