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

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

Proof of Theorem 3adant1r
StepHypRef Expression
1 3adant1l.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213expb 1145 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
32adantlr 462 . 2 (((𝜑𝜏) ∧ (𝜓𝜒)) → 𝜃)
433impb 1140 1 (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 927
This theorem is referenced by:  3adant2r  1170  3adant3r  1172  tfr1onlembacc  6121  tfr1onlembfn  6123  tfr1onlemaccex  6127  tfr1onlemres  6128  tfrcllembfn  6136  tfrcllemaccex  6140  tfrcllemres  6141  tfrcldm  6142  tfrcl  6143  mulassnqg  7004  prarloc  7123  prmuloc  7186  addasssrg  7363  axaddass  7468
  Copyright terms: Public domain W3C validator