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

Theorem adantrr 697
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1 ((φ ψ) → χ)
Assertion
Ref Expression
adantrr ((φ (ψ θ)) → χ)

Proof of Theorem adantrr
StepHypRef Expression
1 simpl 443 . 2 ((ψ θ) → ψ)
2 adant2.1 . 2 ((φ ψ) → χ)
31, 2sylan2 460 1 ((φ (ψ θ)) → χ)
Colors of variables: wff setvar class
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:  ad2ant2r  727  ad2ant2lr  728  consensus  925  3ad2antr1  1120  sbcom  2089  ax11eq  2193  ax11el  2194  nndisjeq  4429  tfinpw1  4494  tfinsuc  4498  sfindbl  4530  vfinspsslem1  4550  isocnv  5491  isores2  5493  isoini  5497  f1oiso2  5500  ncspw1eu  6159  addccan2nc  6265  frecxp  6314  fnfrec  6320
  Copyright terms: Public domain W3C validator