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

Theorem ad2ant2lr 497
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 466 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantll 463 1 (((𝜃𝜑) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  mpteqb  5443  fiunsnnn  6704  addcomnqg  7090  addassnqg  7091  nqtri3or  7105  lt2addnq  7113  lt2mulnq  7114  enq0ref  7142  enq0tr  7143  nqnq0pi  7147  nqpnq0nq  7162  nqnq0a  7163  distrnq0  7168  addassnq0lemcl  7170  ltsrprg  7443  mulcomsrg  7453  mulasssrg  7454  distrsrg  7455  aptisr  7474  mulcnsr  7522  cnegex  7811  sub4  7878  muladd  8013  ltleadd  8075  divdivdivap  8334  divadddivap  8348  ltmul12a  8476  fzrev  9705  facndiv  10326  cncongr1  11577  blbas  12361  cncfmet  12492
  Copyright terms: Public domain W3C validator