![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3simpc | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Ref | Expression |
---|---|
3simpc | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anrot 925 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) | |
2 | 3simpa 936 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒)) | |
3 | 1, 2 | sylbi 119 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: simp3 941 3adant1 957 3adantl1 1095 3adantr1 1098 eupickb 2023 find 4342 eqsupti 6458 divcanap2 7824 diveqap0 7826 divrecap 7832 divcanap3 7842 eliooord 9016 fzrev3 9169 sqdivap 9626 muldvds2 10355 dvdscmul 10356 dvdsmulc 10357 dvdstr 10366 |
Copyright terms: Public domain | W3C validator |