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

Theorem ad2ant2rl 502
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 469 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantlr 468 1 (((𝜑𝜃) ∧ (𝜏𝜓)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  fvtp1g  5628  fcof1o  5690  infnfi  6789  addcomnqg  7196  addassnqg  7197  nqtri3or  7211  ltexnqq  7223  nqnq0pi  7253  nqpnq0nq  7268  nqnq0a  7269  addassnq0lemcl  7276  ltaddpr  7412  ltexprlemloc  7422  addcanprlemu  7430  recexprlem1ssu  7449  aptiprleml  7454  mulcomsrg  7572  mulasssrg  7573  distrsrg  7574  aptisr  7594  mulcnsr  7650  cnegex  7947  muladd  8153  lemul12b  8626  qaddcl  9434  iooshf  9742  elfzomelpfzo  10015  expnegzap  10334  setscom  12009  cnpnei  12398
  Copyright terms: Public domain W3C validator