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  1642  syl5sseq  2993  ssdifin0  3304  uneqdifeqim  3308  unimax  3614  opth  3974  djussxp  4481  iss  4654  relresfld  4847  eldmrexrn  5308  f1oresrab  5329  fmptco  5330  fsn  5335  fnressn  5349  foeqcnvco  5430  isoini2  5458  ofres  5725  ofco  5729  tposexg  5873  tfrlemisucaccv  5939  tfrlemibex  5943  rdgivallem  5968  frecabex  5984  frectfr  5985  frecrdg  5992  en1  6279  2dom  6285  phplem4  6318  archnqq  6513  prarloclemlt  6589  prarloclemlo  6590  prarloclemcalc  6598  recexprlemm  6720  recexprlemex  6733  caucvgprlemm  6764  caucvgprprlemmu  6791  1idsr  6851  recexgt0sr  6856  archsr  6864  caucvgsrlemoffval  6878  caucvgsrlemofff  6879  caucvgsrlemoffres  6882  caucvgsr  6884  pitonnlem2  6921  pitonn  6922  pitoregt0  6923  pitore  6924  recnnre  6925  axrnegex  6951  nntopi  6966  msqge0  7605  mulge0  7608  recexaplem2  7631  recexap  7632  recgt0  7814  recreclt  7864  nn1m1nn  7930  nn1suc  7931  nnle1eq1  7936  nn1gt1  7945  nnsub  7950  addltmul  8159  nn0le0eq0  8208  elnn0nn  8222  elnnz  8253  elznn0  8258  zlem1lt  8298  zltlem1  8299  elz2  8310  nn0n0n1ge2b  8318  nn0lt2  8320  eluzaddi  8497  eluzsubi  8498  uzp1  8504  peano2uzr  8526  nn01to3  8550  qreccl  8574  ltpnf  8700  fz01en  8915  fzpreddisj  8931  fzsuc2  8939  fseq1p1m1  8954  fseq1m1p1  8955  elfzp1b  8957  fzoss2  9026  fzval3  9058  fzosplitsnm1  9063  fzosplitprm1  9088  flhalf  9142  frec2uzrand  9165  frecuzrdgrom  9170  frecuzrdg0  9174  frecfzennn  9177  frecfzen2  9178  iseqeq1  9188  iseqm1  9201  monoord2  9210  isermono  9211  iser0f  9225  expm1t  9257  expeq0  9260  expubnd  9285  binom3  9340  shftfval  9396  2shfti  9406  resqrexlemf1  9580  abs00ap  9634  abs00  9636  sqabs  9652  ltabs  9657  caubnd2  9687  mulcn2  9807  climaddc1  9823  climmulc2  9825  climsubc1  9826  climsubc2  9827  iiserex  9833  climlec2  9835  climcvg1nlem  9842  serif0  9845  nn0seqcvgd  9854  ialgcvg  9861  algcvgblem  9862