![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3simpa | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
3simpa | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 922 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 1 | simplbi 268 | 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 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: 3simpb 937 3simpc 938 simp1 939 simp2 940 3adant3 959 3adantl3 1097 3adantr3 1100 opprc 3612 oprcl 3615 opm 4018 funtpg 5002 ftpg 5401 ovig 5675 prltlu 6816 mullocpr 6900 lt2halves 8410 nn0n0n1ge2 8576 ixxssixx 9078 dvdsmulcr 10458 dvds2add 10462 dvds2sub 10463 dvdstr 10465 bj-peano4 11042 |
Copyright terms: Public domain | W3C validator |