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

Theorem 3adant3r 1198
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 1171 . . 3 ((𝜒𝜓𝜑) → 𝜃)
323adant1r 1194 . 2 (((𝜒𝜏) ∧ 𝜓𝜑) → 𝜃)
433com13 1171 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 947
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 949
This theorem is referenced by:  addassnqg  7158  mulassnqg  7160  prarloc  7279  ltpopr  7371  ltexprlemfl  7385  ltexprlemfu  7387  addasssrg  7532  axaddass  7648  apmul1  8516  ltmul2  8582  lemul2  8583  dvdscmulr  11449  dvdsmulcr  11450  modremain  11553  ndvdsadd  11555  rpexp12i  11760  xblcntrps  12509  xblcntr  12510
  Copyright terms: Public domain W3C validator