ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2ant2rl GIF version

Theorem ad2ant2rl 496
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
Hypothesis
Ref Expression
ad2ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad2ant2rl (((𝜑𝜃) ∧ (𝜏𝜓)) → 𝜒)

Proof of Theorem ad2ant2rl
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrl 463 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantlr 462 1 (((𝜑𝜃) ∧ (𝜏𝜓)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  fvtp1g  5544  fcof1o  5606  infnfi  6691  addcomnqg  7037  addassnqg  7038  nqtri3or  7052  ltexnqq  7064  nqnq0pi  7094  nqpnq0nq  7109  nqnq0a  7110  addassnq0lemcl  7117  ltaddpr  7253  ltexprlemloc  7263  addcanprlemu  7271  recexprlem1ssu  7290  aptiprleml  7295  mulcomsrg  7400  mulasssrg  7401  distrsrg  7402  aptisr  7421  mulcnsr  7469  cnegex  7757  muladd  7959  lemul12b  8419  qaddcl  9219  iooshf  9518  elfzomelpfzo  9791  expnegzap  10104  setscom  11683  cnpnei  12070
  Copyright terms: Public domain W3C validator