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

Theorem adantrl 696
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
adantrl ((φ (θ ψ)) → χ)

Proof of Theorem adantrl
StepHypRef Expression
1 simpr 447 . 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-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:  ad2ant2l  726  ad2ant2rl  729  consensus  925  3ad2antr2  1121  3ad2antr3  1122  sbcom  2089  tfinltfin  4501  evenodddisj  4516  spfininduct  4540  foco  5279  isocnv  5491  isores2  5493  f1oiso2  5500  fvfullfunlem3  5863  clos1induct  5880  weds  5938  ncspw1eu  6159  tlecg  6230  addccan2nc  6265  nchoicelem12  6300  fnfrec  6320
  Copyright terms: Public domain W3C validator