![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3simpb | Structured version Visualization version GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
Ref | Expression |
---|---|
3simpb | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ 𝜒)) | |
2 | 1 | 3adant2 1126 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 df-3an 1074 |
This theorem is referenced by: 3adant2OLD 1153 3adantl2 1173 3adantr2 1176 fpropnf1 6687 cfcof 9288 axcclem 9471 enqeq 9948 ltleletr 10322 ixxssixx 12382 prodmolem2 14864 prodmo 14865 zprod 14866 muldvds1 15208 dvds2add 15217 dvds2sub 15218 dvdstr 15220 initoeu2lem2 16866 pospropd 17335 csrgbinom 18746 smadiadetglem2 20680 ismbf3d 23620 mbfi1flimlem 23688 colinearalg 25989 frusgrnn0 26677 wlkwwlkinj 27005 2wlkond 27057 2pthond 27062 2pthon3v 27063 umgr2adedgwlkonALT 27067 vdgn1frgrv2 27450 frgr2wwlkeqm 27485 bnj967 31322 bnj1110 31357 cgr3permute3 32460 cgr3com 32466 brofs2 32490 areacirclem4 33816 paddasslem14 35622 lhpexle1 35797 cdlemk19w 36762 ismrc 37766 iocinico 38299 gneispb 38931 fourierdlem113 40939 sigaras 41550 sigarms 41551 leltletr 41818 lincresunit3lem3 42773 lincresunit3 42780 |
Copyright terms: Public domain | W3C validator |