![]() |
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 1183 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | adantlr 469 | . 2 ⊢ (((𝜑 ∧ 𝜏) ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
4 | 3 | 3impb 1178 | 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: 3adant2r 1212 3adant3r 1214 tfr1onlembacc 6247 tfr1onlembfn 6249 tfr1onlemaccex 6253 tfr1onlemres 6254 tfrcllembfn 6262 tfrcllemaccex 6266 tfrcllemres 6267 tfrcldm 6268 tfrcl 6269 mulassnqg 7216 prarloc 7335 prmuloc 7398 addasssrg 7588 axaddass 7704 |
Copyright terms: Public domain | W3C validator |