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

Theorem ad2ant2rl 495
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 462 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantlr 461 1 (((𝜑𝜃) ∧ (𝜏𝜓)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  fvtp1g  5401  fcof1o  5460  infnfi  6429  addcomnqg  6633  addassnqg  6634  nqtri3or  6648  ltexnqq  6660  nqnq0pi  6690  nqpnq0nq  6705  nqnq0a  6706  addassnq0lemcl  6713  ltaddpr  6849  ltexprlemloc  6859  addcanprlemu  6867  recexprlem1ssu  6886  aptiprleml  6891  mulcomsrg  6996  mulasssrg  6997  distrsrg  6998  aptisr  7017  mulcnsr  7065  cnegex  7353  muladd  7555  lemul12b  8006  qaddcl  8801  iooshf  9051  elfzomelpfzo  9317  expnegzap  9607
  Copyright terms: Public domain W3C validator