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

Theorem 3adant3r 1143
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant3r ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)

Proof of Theorem 3adant3r
StepHypRef Expression
1 3adant1l.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213com13 1120 . . 3 ((𝜒𝜓𝜑) → 𝜃)
323adant1r 1139 . 2 (((𝜒𝜏) ∧ 𝜓𝜑) → 𝜃)
433com13 1120 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896
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 depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  addassnqg  6538  mulassnqg  6540  prarloc  6659  ltpopr  6751  ltexprlemfl  6765  ltexprlemfu  6767  addasssrg  6899  axaddass  7004  apmul1  7839  ltmul2  7897  lemul2  7898  dvdscmulr  10136  dvdsmulcr  10137  modremain  10241  ndvdsadd  10243
  Copyright terms: Public domain W3C validator