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

Theorem ad2ant2l 485
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 455 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantll 453 1 (((𝜃𝜑) ∧ (𝜏𝜓)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  mpteqb  5289  mpt2fun  5631  xpdom2  6336  addcmpblnq  6523  addpipqqslem  6525  addpipqqs  6526  addclnq  6531  addcomnqg  6537  addassnqg  6538  mulcomnqg  6539  mulassnqg  6540  distrnqg  6543  ltdcnq  6553  enq0ref  6589  addcmpblnq0  6599  addclnq0  6607  nqpnq0nq  6609  nqnq0a  6610  nqnq0m  6611  distrnq0  6615  mulcomnq0  6616  addassnq0lemcl  6617  genpdisj  6679  appdiv0nq  6720  addcomsrg  6898  mulcomsrg  6900  mulasssrg  6901  distrsrg  6902  addcnsr  6968  mulcnsr  6969  addcnsrec  6976  axaddcl  6998  axmulcl  7000  axaddcom  7002  add42  7236  muladd  7453  mulsub  7470  apreim  7668  divmuleqap  7768  ltmul12a  7901  lemul12b  7902  lemul12a  7903  qaddcl  8667  qmulcl  8669  iooshf  8922  fzass4  9027  elfzomelpfzo  9189
  Copyright terms: Public domain W3C validator