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  5596  fcof1o  5658  infnfi  6757  addcomnqg  7157  addassnqg  7158  nqtri3or  7172  ltexnqq  7184  nqnq0pi  7214  nqpnq0nq  7229  nqnq0a  7230  addassnq0lemcl  7237  ltaddpr  7373  ltexprlemloc  7383  addcanprlemu  7391  recexprlem1ssu  7410  aptiprleml  7415  mulcomsrg  7533  mulasssrg  7534  distrsrg  7535  aptisr  7555  mulcnsr  7611  cnegex  7908  muladd  8114  lemul12b  8587  qaddcl  9395  iooshf  9703  elfzomelpfzo  9976  expnegzap  10295  setscom  11926  cnpnei  12315
  Copyright terms: Public domain W3C validator