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

Theorem ad2ant2lr 510
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 479 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantll 476 1 (((𝜃𝜑) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  mpteqb  5649  fiunsnnn  6939  addcomnqg  7443  addassnqg  7444  nqtri3or  7458  lt2addnq  7466  lt2mulnq  7467  enq0ref  7495  enq0tr  7496  nqnq0pi  7500  nqpnq0nq  7515  nqnq0a  7516  distrnq0  7521  addassnq0lemcl  7523  ltsrprg  7809  mulcomsrg  7819  mulasssrg  7820  distrsrg  7821  aptisr  7841  mulcnsr  7897  cnegex  8199  sub4  8266  muladd  8405  ltleadd  8467  divdivdivap  8734  divadddivap  8748  ltmul12a  8881  fzrev  10153  facndiv  10813  cncongr1  12244  ghmeql  13340  blbas  14612  cncfmet  14771  ptolemy  15000
  Copyright terms: Public domain W3C validator