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 964 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 1 | simplbi 272 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: 3simpb 979 3simpc 980 simp1 981 simp2 982 3adant3 1001 3adantl3 1139 3adantr3 1142 opprc 3726 oprcl 3729 opm 4156 funtpg 5174 ftpg 5604 ovig 5892 prltlu 7295 mullocpr 7379 lt2halves 8955 nn0n0n1ge2 9121 ixxssixx 9685 sumtp 11183 dvdsmulcr 11523 dvds2add 11527 dvds2sub 11528 dvdstr 11530 bj-peano4 13153 |
Copyright terms: Public domain | W3C validator |