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

Theorem ad2antrr 706
 Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
Hypothesis
Ref Expression
ad2ant.1 (φψ)
Assertion
Ref Expression
ad2antrr (((φ χ) θ) → ψ)

Proof of Theorem ad2antrr
StepHypRef Expression
1 ad2ant.1 . . 3 (φψ)
21adantr 451 . 2 ((φ θ) → ψ)
32adantlr 695 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:  ad3antrrr  710  simpll  730  simplll  734  simpllr  735  ax11eq  2193  ax11el  2194  ax11indalem  2197  ax11inda2ALT  2198  vtoclgft  2905  reupick  3539  ltfinasym  4460  sfinltfin  4535  vfinspsslem1  4550  isotr  5495  qsdisj  5995  nntccl  6170  sbthlem3  6205  ltlenlec  6207  letc  6231  ncslemuc  6255  fnfrec  6320
 Copyright terms: Public domain W3C validator