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

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

Proof of Theorem ad2ant2lr
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrr 456 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantll 453 1 (((𝜃𝜑) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  mpteqb  5288  fiunsnnn  6368  addcomnqg  6536  addassnqg  6537  nqtri3or  6551  lt2addnq  6559  lt2mulnq  6560  enq0ref  6588  enq0tr  6589  nqnq0pi  6593  nqpnq0nq  6608  nqnq0a  6609  distrnq0  6614  addassnq0lemcl  6616  ltsrprg  6889  mulcomsrg  6899  mulasssrg  6900  distrsrg  6901  aptisr  6920  mulcnsr  6968  cnegex  7251  sub4  7318  muladd  7452  ltleadd  7514  divdivdivap  7763  divadddivap  7777  ltmul12a  7900  fzrev  9047  facndiv  9606
  Copyright terms: Public domain W3C validator