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.) |
Ref | Expression |
---|---|
simprr1 | ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr1 1060 | . 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: sqrmo 13840 icodiamlt 14022 psgnunilem2 17738 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 hauspwpwf1 21601 itg2add 23332 ulmdvlem3 23960 ax5seglem6 25614 frg2woteqm 26586 numclwlk1lem2f 26619 numclwwlk5 26639 conpcon 30471 cvmliftmolem2 30518 cvmlift2lem10 30548 cvmlift3lem2 30556 cvmlift3lem8 30562 broutsideof3 31403 unblimceq0 31668 paddasslem10 34133 lhpexle2lem 34313 lhpexle3lem 34315 cdlemj3 35129 cdlemkid4 35240 mpaaeu 36739 stoweidlem35 38928 stoweidlem56 38949 stoweidlem59 38952 fusgrfis 40549 umgr2wlkon 41157 av-numclwlk1lem2f 41522 av-numclwwlk5 41542 |
Copyright terms: Public domain | W3C validator |