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  recexprlemm  6595  recexprlemex  6608  1idsr  6676  recexgt0sr  6681  archsr  6688  pitonnlem2  6723  pitonn  6724  axrnegex  6743  msqge0  7380  mulge0  7383  recexaplem2  7395  recexap  7396  recgt0  7577  recreclt  7627  nn1m1nn  7693  nn1suc  7694  nnle1eq1  7699  nn1gt1  7708  nnsub  7713  addltmul  7918  nn0le0eq0  7966  elnn0nn  7980  elnnz  8011  elznn0  8016  zlem1lt  8056  zltlem1  8057  elz2  8068  nn0n0n1ge2b  8076  nn0lt2  8078  eluzaddi  8255  eluzsubi  8256  uzp1  8262  peano2uzr  8284  nn01to3  8308  qreccl  8331  ltpnf  8452  fz01en  8667  fzpreddisj  8683  fzsuc2  8691  fseq1p1m1  8706  fseq1m1p1  8707  elfzp1b  8709  fzoss2  8778  fzval3  8810  fzosplitsnm1  8815  fzosplitprm1  8840  frec2uzrand  8852  frecuzrdgrom  8857  frecuzrdg0  8861  frecfzennn  8864  frecfzen2  8865  iseqeq1  8874  expm1t  8917  expeq0  8920  expubnd  8945  binom3  8999