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

Theorem 3adant3r 1214
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 1187 . . 3 ((𝜒𝜓𝜑) → 𝜃)
323adant1r 1210 . 2 (((𝜒𝜏) ∧ 𝜓𝜑) → 𝜃)
433com13 1187 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963
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 965
This theorem is referenced by:  addassnqg  7213  mulassnqg  7215  prarloc  7334  ltpopr  7426  ltexprlemfl  7440  ltexprlemfu  7442  addasssrg  7587  axaddass  7703  apmul1  8571  ltmul2  8637  lemul2  8638  dvdscmulr  11556  dvdsmulcr  11557  modremain  11660  ndvdsadd  11662  rpexp12i  11867  xblcntrps  12619  xblcntr  12620
  Copyright terms: Public domain W3C validator