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

Theorem 3ad2antl1 1143
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1 ((𝜑𝜒) → 𝜃)
Assertion
Ref Expression
3ad2antl1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3ad2antl1
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantlr 468 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl2 1138 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 962
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 depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  acexmid  5776  ordiso2  6923  addlocpr  7363  distrlem1prl  7409  distrlem1pru  7410  ltsopr  7423  addcanprlemu  7442  fzo1fzo0n0  9984  prodfap0  11338  prodfrecap  11339  muldvds2  11542  dvds2add  11550  dvds2sub  11551  dvdstr  11553  cnpnei  12414  upxp  12467
  Copyright terms: Public domain W3C validator