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

Theorem adantrd 454
Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
Hypothesis
Ref Expression
adantrd.1 (φ → (ψχ))
Assertion
Ref Expression
adantrd (φ → ((ψ θ) → χ))

Proof of Theorem adantrd
StepHypRef Expression
1 simpl 443 . 2 ((ψ θ) → ψ)
2 adantrd.1 . 2 (φ → (ψχ))
31, 2syl5 28 1 (φ → ((ψ θ) → χ))
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  syldan  456  jaoa  496  prlem1  928  cad0  1400  equveli  1988  2eu3  2286  unineq  3505  tfinltfinlem1  4500  sfintfin  4532  vfinncvntnn  4548  fvun1  5379  fnasrn  5417  fconst5  5455  fconstfv  5456  enadjlem1  6059  leltctr  6212  addcdi  6250  nmembers1lem3  6270  nchoicelem12  6300
  Copyright terms: Public domain W3C validator