![]() |
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 980 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 1 | simplbi 274 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 3simpb 995 3simpc 996 simp1 997 simp2 998 3adant3 1017 3adantl3 1155 3adantr3 1158 opprc 3797 oprcl 3800 opm 4230 funtpg 5262 ftpg 5695 ovig 5989 prltlu 7464 mullocpr 7548 lt2halves 9130 nn0n0n1ge2 9299 ixxssixx 9876 sumtp 11393 dvdsmulcr 11799 dvds2add 11803 dvds2sub 11804 dvdstr 11806 dfgrp3me 12846 bj-peano4 14329 |
Copyright terms: Public domain | W3C validator |