Theorem 3adant3 975

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
3adant3	⊢ ((φ ∧ ψ ∧ θ) → χ)

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 952	. 2 ⊢ ((φ ∧ ψ ∧ θ) → (φ ∧ ψ))
2		3adant.1	. 2 ⊢ ((φ ∧ ψ) → χ)
3	1, 2	syl 15	1 ⊢ ((φ ∧ ψ ∧ θ) → χ)

Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934

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  df-3an 936

This theorem is referenced by:  vtoclgft  2905  eqeu  3007  sikss1c1c  4267  ins2kss  4279  ins3kss  4280  leltfintr  4458  ltfintr  4459  lefinlteq  4463  ltfintri  4466  ncfineleq  4477  tfindi  4496  tfinltfin  4501  sfintfin  4532  tfinnn  4534  spfinsfincl  4539  addccan2  4559  brsi  4761  fnco  5191  resdif  5306  fnimapr  5374  f1ocnvfvb  5479  f1oiso2  5500  fununiq  5517  ovig  5597  ov2ag  5598  ov6g  5600  ovg  5601  ovmpt2x  5712  elmapg  6012  elpmg  6013  ceclr  6187  addlec  6208  lectr  6211  leaddc1  6214  nclenn  6249  addcdir  6251  lemuc1  6253  ncslemuc  6255  lecadd2  6266  spaccl  6286