![]() |
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 1138 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | ad2antll 727 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 397 df-3an 1089 |
This theorem is referenced by: el2xptp0 7960 poxp2 8067 ttrcltr 9610 icodiamlt 15274 psgnunilem2 19230 srgbinom 19910 psgndiflemA 20952 haust1 22649 cnhaus 22651 isreg2 22674 llynlly 22774 restnlly 22779 llyrest 22782 llyidm 22785 nllyidm 22786 cldllycmp 22792 txlly 22933 txnlly 22934 pthaus 22935 txhaus 22944 txkgen 22949 xkohaus 22950 xkococnlem 22956 cmetcaulem 24598 itg2add 25070 ulmdvlem3 25707 nosupprefixmo 26994 noinfprefixmo 26995 nosupno 26997 noinfno 27012 etasslt 27098 scutbdaybnd 27100 scutbdaybnd2 27101 ax5seglem6 27728 fusgrfis 28123 wwlksnextfun 28688 umgr2wlkon 28740 connpconn 33657 cvmlift3lem2 33742 cvmlift3lem8 33748 addsproplem6 34283 negsproplem6 34320 ifscgr 34561 broutsideof3 34643 unblimceq0 34902 paddasslem10 38224 lhpexle2lem 38404 lhpexle3lem 38406 mpaaeu 41380 stoweidlem35 44171 stoweidlem56 44192 stoweidlem59 44195 |
Copyright terms: Public domain | W3C validator |