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

Theorem 3ad2antl1 1159
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 477 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl2 1154 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:  acexmid  5867  ordiso2  7027  addlocpr  7513  distrlem1prl  7559  distrlem1pru  7560  ltsopr  7573  addcanprlemu  7592  fzo1fzo0n0  10156  prodfap0  11524  prodfrecap  11525  muldvds2  11795  dvds2add  11803  dvds2sub  11804  dvdstr  11806  mulgnnsubcl  12871  mulgpropdg  12900  ringidss  13025  cnpnei  13352  upxp  13405  lgsval4lem  14045
  Copyright terms: Public domain W3C validator