![]() |
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 1137 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antll 728 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: poxp2 8129 sqrmo 15198 icodiamlt 15382 psgnunilem2 19363 haust1 22856 cnhaus 22858 isreg2 22881 llynlly 22981 restnlly 22986 llyrest 22989 llyidm 22992 nllyidm 22993 cldllycmp 22999 txlly 23140 txnlly 23141 pthaus 23142 txhaus 23151 txkgen 23156 xkohaus 23157 xkococnlem 23163 hauspwpwf1 23491 itg2add 25277 ulmdvlem3 25914 nosupno 27206 noinfno 27221 etasslt 27314 scutbdaybnd 27316 scutbdaybnd2 27317 addsproplem6 27458 negsproplem6 27507 mulsproplem13 27584 mulsproplem14 27585 mulsprop 27586 ax5seglem6 28192 fusgrfis 28587 umgr2wlkon 29204 numclwwlk5 29641 connpconn 34226 cvmliftmolem2 34273 cvmlift2lem10 34303 cvmlift3lem2 34311 cvmlift3lem8 34317 broutsideof3 35098 unblimceq0 35383 paddasslem10 38700 lhpexle2lem 38880 lhpexle3lem 38882 cdlemj3 39694 cdlemkid4 39805 mpaaeu 41892 stoweidlem35 44751 stoweidlem56 44772 stoweidlem59 44775 |
Copyright terms: Public domain | W3C validator |