Theorem syl2an 463

Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)

Hypotheses

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

Assertion

Ref	Expression
syl2an	⊢ ((φ ∧ τ) → θ)

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		syl2an.2	. 2 ⊢ (τ → χ)
2		syl2an.1	. . 3 ⊢ (φ → ψ)
3		syl2an.3	. . 3 ⊢ ((ψ ∧ χ) → θ)
4	2, 3	sylan 457	. 2 ⊢ ((φ ∧ χ) → θ)
5	1, 4	sylan2 460	1 ⊢ ((φ ∧ τ) → θ)

Syntax hints:   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  syl2anr  464  anim12i  549  ax11indalem  2197  eqeqan12d  2368  sylan9eq  2405  csbcomg  3159  sylan9ss  3285  ssconb  3399  ineqan12d  3459  ifpr  3774  unexg  4101  opkelopkabg  4245  opkelcokg  4261  opkelimagekg  4271  xpkexg  4288  cokexg  4309  ncfinlower  4483  tfindi  4496  tfinlefin  4502  vfinspsslem1  4550  opexg  4587  copsex2g  4609  breqan12d  4654  coexg  4749  opbrop  4841  dmpropg  5068  xpexg  5114  funssres  5144  fnco  5191  fcnvres  5243  fodmrnu  5277  fvun1  5379  fconst2g  5452  isomin  5496  oveqan12d  5541  ovg  5601  txpexg  5784  cupvalg  5812  pprodexg  5837  ovcross  5845  qsexg  5982  mapvalg  6009  pmvalg  6010  mapsn  6026  xpassen  6057  enmap1lem5  6073  enprmaplem3  6078  ncaddccl  6144  ncdisjeq  6148  ovcelem1  6171  cenc  6181  sbthlem1  6203  sbthlem3  6205  lectr  6211  leconnnc  6218  tlecg  6230  nmembers1lem3  6270  nnc3n3p1  6278  nnc3n3p2  6279  nnc3p1n3p2  6280  nchoicelem5  6293  nchoicelem17  6305