![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simprr1 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
Ref | Expression |
---|---|
simprr1 | ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1136 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antll 727 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: poxp2 8074 sqrmo 15135 icodiamlt 15319 psgnunilem2 19275 haust1 22701 cnhaus 22703 isreg2 22726 llynlly 22826 restnlly 22831 llyrest 22834 llyidm 22837 nllyidm 22838 cldllycmp 22844 txlly 22985 txnlly 22986 pthaus 22987 txhaus 22996 txkgen 23001 xkohaus 23002 xkococnlem 23008 hauspwpwf1 23336 itg2add 25122 ulmdvlem3 25759 nosupno 27049 noinfno 27064 etasslt 27150 scutbdaybnd 27152 scutbdaybnd2 27153 addsproplem6 27284 negsproplem6 27329 ax5seglem6 27881 fusgrfis 28276 umgr2wlkon 28893 numclwwlk5 29330 connpconn 33820 cvmliftmolem2 33867 cvmlift2lem10 33897 cvmlift3lem2 33905 cvmlift3lem8 33911 broutsideof3 34702 unblimceq0 34961 paddasslem10 38283 lhpexle2lem 38463 lhpexle3lem 38465 cdlemj3 39277 cdlemkid4 39388 mpaaeu 41455 stoweidlem35 44248 stoweidlem56 44269 stoweidlem59 44272 |
Copyright terms: Public domain | W3C validator |