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

Theorem 3adant2 974
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1 ((φ ψ) → χ)
Assertion
Ref Expression
3adant2 ((φ θ ψ) → χ)

Proof of Theorem 3adant2
StepHypRef Expression
1 3simpb 953 . 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:  3ad2ant1  976  eupickb  2269  vtoclegft  2926  eqeu  3007  leltfintr  4458  ltfintr  4459  ltfintri  4466  ncfineleq  4477  tfinltfin  4501  vfinspnn  4541  vfintle  4546  phi11lem1  4595  fnco  5191  dff1o2  5291  fnimapr  5374  f1elima  5474  f1ocnvfvb  5479  fununiq  5517  oprssov  5603  ncspw1eu  6159  leaddc1  6214  letc  6231  addcdir  6251  lemuc1  6253  lecadd2  6266  nchoicelem17  6305
  Copyright terms: Public domain W3C validator