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  6475  prarloclemlo  6476  prarloclemcalc  6484  addnqpr1lemrl  6537  addnqpr1lemru  6538  addnqpr1lemil  6539  addnqpr1lemiu  6540  addnqpr1  6541  recexprlemm  6594  recexprlemex  6607  1idsr  6656  recexgt0sr  6661  archsr  6668  pitonnlem2  6703  pitonn  6704  axrnegex  6723  msqge0  7360  mulge0  7363  recexaplem2  7375  recexap  7376  recgt0  7557  recreclt  7607  nn1m1nn  7673  nn1suc  7674  nnle1eq1  7679  nn1gt1  7688  nnsub  7693  addltmul  7898  nn0le0eq0  7946  elnn0nn  7960  elnnz  7991  elznn0  7996  zlem1lt  8036  zltlem1  8037  elz2  8048  nn0n0n1ge2b  8056  nn0lt2  8058  eluzaddi  8235  eluzsubi  8236  uzp1  8242  peano2uzr  8264  nn01to3  8288  qreccl  8311  ltpnf  8432  fz01en  8647  fzpreddisj  8663  fzsuc2  8671  fseq1p1m1  8686  fseq1m1p1  8687  elfzp1b  8689  fzoss2  8758  fzval3  8790  fzosplitsnm1  8795  fzosplitprm1  8820  frec2uzrand  8832  frecuzrdgrom  8837  frecuzrdg0  8841  frecfzennn  8844  frecfzen2  8845  iseqeq1  8854  expm1t  8897  expeq0  8900  expubnd  8925  binom3  8979