![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simprr3 | 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 |
---|---|
simprr3 | ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 1139 | . 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: el2xptp0 8022 poxp2 8129 ttrcltr 9711 icodiamlt 15382 psgnunilem2 19363 srgbinom 20054 psgndiflemA 21154 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 cmetcaulem 24805 itg2add 25277 ulmdvlem3 25914 nosupprefixmo 27203 noinfprefixmo 27204 nosupno 27206 noinfno 27221 etasslt 27314 scutbdaybnd 27316 scutbdaybnd2 27317 addsproplem6 27458 negsproplem6 27507 mulsproplem13 27584 mulsproplem14 27585 mulsprop 27586 ax5seglem6 28192 fusgrfis 28587 wwlksnextfun 29152 umgr2wlkon 29204 connpconn 34226 cvmlift3lem2 34311 cvmlift3lem8 34317 ifscgr 35016 broutsideof3 35098 unblimceq0 35383 paddasslem10 38700 lhpexle2lem 38880 lhpexle3lem 38882 mpaaeu 41892 stoweidlem35 44751 stoweidlem56 44772 stoweidlem59 44775 |
Copyright terms: Public domain | W3C validator |