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

Theorem ad2ant2l 497
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 467 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantll 465 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  5477  mpofun  5839  xpdom2  6691  addcmpblnq  7139  addpipqqslem  7141  addpipqqs  7142  addclnq  7147  addcomnqg  7153  addassnqg  7154  mulcomnqg  7155  mulassnqg  7156  distrnqg  7159  ltdcnq  7169  enq0ref  7205  addcmpblnq0  7215  addclnq0  7223  nqpnq0nq  7225  nqnq0a  7226  nqnq0m  7227  distrnq0  7231  mulcomnq0  7232  addassnq0lemcl  7233  genpdisj  7295  appdiv0nq  7336  addcomsrg  7527  mulcomsrg  7529  mulasssrg  7530  distrsrg  7531  addcnsr  7606  mulcnsr  7607  addcnsrec  7614  axaddcl  7636  axmulcl  7638  axaddcom  7642  add42  7888  muladd  8110  mulsub  8127  apreim  8328  divmuleqap  8440  ltmul12a  8578  lemul12b  8579  lemul12a  8580  qaddcl  9379  qmulcl  9381  iooshf  9686  fzass4  9793  elfzomelpfzo  9959  tanaddaplem  11355  opnneissb  12230  neitx  12343  txcnmpt  12348  txrest  12351  metcnp3  12586  cncfmet  12654  dveflem  12761
  Copyright terms: Public domain W3C validator