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 924 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) | |
2 | 3simpa 935 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒)) | |
3 | 1, 2 | sylbi 119 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 919 |
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 921 |
This theorem is referenced by: simp3 940 3adant1 956 3adantl1 1094 3adantr1 1097 eupickb 2022 find 4340 eqsupti 6409 divcanap2 7768 diveqap0 7770 divrecap 7776 divcanap3 7786 eliooord 8951 fzrev3 9104 sqdivap 9540 muldvds2 10221 dvdscmul 10222 dvdsmulc 10223 dvdstr 10232 |
Copyright terms: Public domain | W3C validator |