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

Theorem ad2ant2lr 501
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 470 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantll 467 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:  mpteqb  5511  fiunsnnn  6775  addcomnqg  7201  addassnqg  7202  nqtri3or  7216  lt2addnq  7224  lt2mulnq  7225  enq0ref  7253  enq0tr  7254  nqnq0pi  7258  nqpnq0nq  7273  nqnq0a  7274  distrnq0  7279  addassnq0lemcl  7281  ltsrprg  7567  mulcomsrg  7577  mulasssrg  7578  distrsrg  7579  aptisr  7599  mulcnsr  7655  cnegex  7952  sub4  8019  muladd  8158  ltleadd  8220  divdivdivap  8485  divadddivap  8499  ltmul12a  8630  fzrev  9876  facndiv  10497  cncongr1  11795  blbas  12616  cncfmet  12762  ptolemy  12927
  Copyright terms: Public domain W3C validator