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  5619  fiunsnnn  6895  addcomnqg  7394  addassnqg  7395  nqtri3or  7409  lt2addnq  7417  lt2mulnq  7418  enq0ref  7446  enq0tr  7447  nqnq0pi  7451  nqpnq0nq  7466  nqnq0a  7467  distrnq0  7472  addassnq0lemcl  7474  ltsrprg  7760  mulcomsrg  7770  mulasssrg  7771  distrsrg  7772  aptisr  7792  mulcnsr  7848  cnegex  8149  sub4  8216  muladd  8355  ltleadd  8417  divdivdivap  8684  divadddivap  8698  ltmul12a  8831  fzrev  10098  facndiv  10733  cncongr1  12117  ghmeql  13161  blbas  14286  cncfmet  14432  ptolemy  14598
  Copyright terms: Public domain W3C validator