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

Theorem 3adant3r 1169
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 1146 . . 3 ((𝜒𝜓𝜑) → 𝜃)
323adant1r 1165 . 2 (((𝜒𝜏) ∧ 𝜓𝜑) → 𝜃)
433com13 1146 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  addassnqg  6885  mulassnqg  6887  prarloc  7006  ltpopr  7098  ltexprlemfl  7112  ltexprlemfu  7114  addasssrg  7246  axaddass  7351  apmul1  8194  ltmul2  8252  lemul2  8253  dvdscmulr  10700  dvdsmulcr  10701  modremain  10804  ndvdsadd  10806  rpexp12i  11009
  Copyright terms: Public domain W3C validator