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

Theorem ad2ant2l 492
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad2ant2l (((𝜃𝜑) ∧ (𝜏𝜓)) → 𝜒)

Proof of Theorem ad2ant2l
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrl 462 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantll 460 1 (((𝜃𝜑) ∧ (𝜏𝜓)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  mpteqb  5358  mpt2fun  5706  xpdom2  6501  addcmpblnq  6873  addpipqqslem  6875  addpipqqs  6876  addclnq  6881  addcomnqg  6887  addassnqg  6888  mulcomnqg  6889  mulassnqg  6890  distrnqg  6893  ltdcnq  6903  enq0ref  6939  addcmpblnq0  6949  addclnq0  6957  nqpnq0nq  6959  nqnq0a  6960  nqnq0m  6961  distrnq0  6965  mulcomnq0  6966  addassnq0lemcl  6967  genpdisj  7029  appdiv0nq  7070  addcomsrg  7248  mulcomsrg  7250  mulasssrg  7251  distrsrg  7252  addcnsr  7318  mulcnsr  7319  addcnsrec  7326  axaddcl  7348  axmulcl  7350  axaddcom  7352  add42  7591  muladd  7809  mulsub  7826  apreim  8024  divmuleqap  8126  ltmul12a  8259  lemul12b  8260  lemul12a  8261  qaddcl  9055  qmulcl  9057  iooshf  9305  fzass4  9410  elfzomelpfzo  9573
  Copyright terms: Public domain W3C validator