Theorem sylancl 392

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

Hypotheses

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

Assertion

Ref	Expression
sylancl	⊢ (φ → θ)

Proof of Theorem sylancl

Step	Hyp	Ref	Expression
1		sylancl.1	. 2 ⊢ (φ → ψ)
2		sylancl.2	. . 3 ⊢ χ
3	2	a1i 9	. 2 ⊢ (φ → χ)
4		sylancl.3	. 2 ⊢ ((ψ ∧ χ) → θ)
5	1, 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:  equveli  1639  syl5sseq  2987  ssdifin0  3298  uneqdifeqim  3302  unimax  3605  opth  3965  djussxp  4424  iss  4597  relresfld  4790  eldmrexrn  5251  f1oresrab  5272  fmptco  5273  fsn  5278  fnressn  5292  foeqcnvco  5373  isoini2  5401  ofres  5667  ofco  5671  tposexg  5814  tfrlemisucaccv  5880  tfrlemibex  5884  rdgivallem  5908  frecabex  5923  frectfr  5924  frecrdg  5931  en1  6215  2dom  6221  archnqq  6400  prarloclemlt  6476  prarloclemlo  6477  prarloclemcalc  6485  recexprlemm  6596  recexprlemex  6609  caucvgprlemm  6639  1idsr  6696  recexgt0sr  6701  archsr  6708  pitonnlem2  6743  pitonn  6744  axrnegex  6763  msqge0  7400  mulge0  7403  recexaplem2  7415  recexap  7416  recgt0  7597  recreclt  7647  nn1m1nn  7713  nn1suc  7714  nnle1eq1  7719  nn1gt1  7728  nnsub  7733  addltmul  7938  nn0le0eq0  7986  elnn0nn  8000  elnnz  8031  elznn0  8036  zlem1lt  8076  zltlem1  8077  elz2  8088  nn0n0n1ge2b  8096  nn0lt2  8098  eluzaddi  8275  eluzsubi  8276  uzp1  8282  peano2uzr  8304  nn01to3  8328  qreccl  8351  ltpnf  8472  fz01en  8687  fzpreddisj  8703  fzsuc2  8711  fseq1p1m1  8726  fseq1m1p1  8727  elfzp1b  8729  fzoss2  8798  fzval3  8830  fzosplitsnm1  8835  fzosplitprm1  8860  frec2uzrand  8872  frecuzrdgrom  8877  frecuzrdg0  8881  frecfzennn  8884  frecfzen2  8885  iseqeq1  8894  expm1t  8937  expeq0  8940  expubnd  8965  binom3  9019