![]() |
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 1129 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antll 725 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 |
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 208 df-an 397 df-3an 1082 |
This theorem is referenced by: sqrmo 14449 icodiamlt 14633 psgnunilem2 18358 haust1 21648 cnhaus 21650 isreg2 21673 llynlly 21773 restnlly 21778 llyrest 21781 llyidm 21784 nllyidm 21785 cldllycmp 21791 txlly 21932 txnlly 21933 pthaus 21934 txhaus 21943 txkgen 21948 xkohaus 21949 xkococnlem 21955 hauspwpwf1 22283 itg2add 24047 ulmdvlem3 24677 ax5seglem6 26407 fusgrfis 26799 umgr2wlkon 27415 numclwwlk5 27855 connpconn 32092 cvmliftmolem2 32139 cvmlift2lem10 32169 cvmlift3lem2 32177 cvmlift3lem8 32183 nosupno 32814 scutbdaybnd 32886 broutsideof3 33198 unblimceq0 33457 paddasslem10 36517 lhpexle2lem 36697 lhpexle3lem 36699 cdlemj3 37511 cdlemkid4 37622 mpaaeu 39256 stoweidlem35 41884 stoweidlem56 41905 stoweidlem59 41908 |
Copyright terms: Public domain | W3C validator |