NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  3adant3 GIF version

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
StepHypRef Expression
1 3simpa 952 . 2 ((φ ψ θ) → (φ ψ))
2 3adant.1 . 2 ((φ ψ) → χ)
31, 2syl 15 1 ((φ ψ θ) → χ)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator