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 972 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) | |
2 | 3simpa 983 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒)) | |
3 | 1, 2 | sylbi 120 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 967 |
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 969 |
This theorem is referenced by: simp3 988 3adant1 1004 3adantl1 1142 3adantr1 1145 eupickb 2094 find 4570 fisseneq 6888 eqsupti 6952 divcanap2 8567 diveqap0 8569 divrecap 8575 divcanap3 8585 eliooord 9855 fzrev3 10012 sqdivap 10509 muldvds2 11743 dvdscmul 11744 dvdsmulc 11745 dvdstr 11754 cncfmptc 13129 cnplimclemr 13185 |
Copyright terms: Public domain | W3C validator |