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.) |
Ref | Expression |
---|---|
simprr3 | ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr3 1069 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒) | |
2 | 1 | adantl 482 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 |
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 386 df-3an 1039 |
This theorem is referenced by: el2xptp0 7212 icodiamlt 14174 psgnunilem2 17915 srgbinom 18545 psgndiflemA 19947 haust1 21156 cnhaus 21158 isreg2 21181 llynlly 21280 restnlly 21285 llyrest 21288 llyidm 21291 nllyidm 21292 cldllycmp 21298 txlly 21439 txnlly 21440 pthaus 21441 txhaus 21450 txkgen 21455 xkohaus 21456 xkococnlem 21462 cmetcaulem 23086 itg2add 23526 ulmdvlem3 24156 ax5seglem6 25814 fusgrfis 26222 wwlksnextfun 26793 umgr2wlkon 26846 connpconn 31217 cvmlift3lem2 31302 cvmlift3lem8 31308 noprefixmo 31848 nosupno 31849 scutbdaybnd 31921 ifscgr 32151 broutsideof3 32233 unblimceq0 32498 paddasslem10 35115 lhpexle2lem 35295 lhpexle3lem 35297 mpaaeu 37720 stoweidlem35 40252 stoweidlem56 40273 stoweidlem59 40276 |
Copyright terms: Public domain | W3C validator |