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

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

Proof of Theorem 3ad2antl2
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantlr 477 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl1 1153 1 (((𝜓𝜑𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  fcofo  5787  cocan1  5790  acexmid  5876  caovimo  6070  ordiso2  7036  mkvprop  7158  ltpopr  7596  ltsopr  7597  addcanprleml  7615  addcanprlemu  7616  aptiprlemu  7641  dvdsmodexp  11804  muldvds1  11825  lcmdvds  12081  cnpnei  13804
  Copyright terms: Public domain W3C validator