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

Theorem 3ad2antl2 1155
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 474 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl1 1148 1 (((𝜓𝜑𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 973
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 975
This theorem is referenced by:  fcofo  5763  cocan1  5766  acexmid  5852  caovimo  6046  ordiso2  7012  mkvprop  7134  ltpopr  7557  ltsopr  7558  addcanprleml  7576  addcanprlemu  7577  aptiprlemu  7602  dvdsmodexp  11757  muldvds1  11778  lcmdvds  12033  cnpnei  13013
  Copyright terms: Public domain W3C validator