Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3adant1r | GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
3adant1l.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant1r | ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3adant1l.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3expb 1182 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | adantlr 468 | . 2 ⊢ (((𝜑 ∧ 𝜏) ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
4 | 3 | 3impb 1177 | 1 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 962 |
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 964 |
This theorem is referenced by: 3adant2r 1211 3adant3r 1213 tfr1onlembacc 6232 tfr1onlembfn 6234 tfr1onlemaccex 6238 tfr1onlemres 6239 tfrcllembfn 6247 tfrcllemaccex 6251 tfrcllemres 6252 tfrcldm 6253 tfrcl 6254 mulassnqg 7185 prarloc 7304 prmuloc 7367 addasssrg 7557 axaddass 7673 |
Copyright terms: Public domain | W3C validator |