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 1062 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒) | |
2 | 1 | adantl 481 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: el2xptp0 7103 icodiamlt 14022 psgnunilem2 17738 srgbinom 18368 psgndiflemA 19766 haust1 20966 cnhaus 20968 isreg2 20991 llynlly 21090 restnlly 21095 llyrest 21098 llyidm 21101 nllyidm 21102 cldllycmp 21108 txlly 21249 txnlly 21250 pthaus 21251 txhaus 21260 txkgen 21265 xkohaus 21266 xkococnlem 21272 cmetcaulem 22894 itg2add 23332 ulmdvlem3 23960 ax5seglem6 25614 wwlkextfun 26257 frg2woteqm 26586 conpcon 30471 cvmlift3lem2 30556 cvmlift3lem8 30562 ifscgr 31321 broutsideof3 31403 unblimceq0 31668 paddasslem10 34133 lhpexle2lem 34313 lhpexle3lem 34315 mpaaeu 36739 stoweidlem35 38928 stoweidlem56 38949 stoweidlem59 38952 fusgrfis 40549 wwlksnextfun 41104 umgr2wlkon 41157 |
Copyright terms: Public domain | W3C validator |