![]() |
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 1089 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒) | |
2 | 1 | adantl 481 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 |
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 385 df-3an 1056 |
This theorem is referenced by: el2xptp0 7256 icodiamlt 14218 psgnunilem2 17961 srgbinom 18591 psgndiflemA 19995 haust1 21204 cnhaus 21206 isreg2 21229 llynlly 21328 restnlly 21333 llyrest 21336 llyidm 21339 nllyidm 21340 cldllycmp 21346 txlly 21487 txnlly 21488 pthaus 21489 txhaus 21498 txkgen 21503 xkohaus 21504 xkococnlem 21510 cmetcaulem 23132 itg2add 23571 ulmdvlem3 24201 ax5seglem6 25859 fusgrfis 26267 wwlksnextfun 26861 umgr2wlkon 26915 connpconn 31343 cvmlift3lem2 31428 cvmlift3lem8 31434 noprefixmo 31973 nosupno 31974 scutbdaybnd 32046 ifscgr 32276 broutsideof3 32358 unblimceq0 32623 paddasslem10 35433 lhpexle2lem 35613 lhpexle3lem 35615 mpaaeu 38037 stoweidlem35 40570 stoweidlem56 40591 stoweidlem59 40594 |
Copyright terms: Public domain | W3C validator |