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 1130 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | ad2antll 725 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: el2xptp0 7725 icodiamlt 14783 psgnunilem2 18552 srgbinom 19224 psgndiflemA 20673 haust1 21888 cnhaus 21890 isreg2 21913 llynlly 22013 restnlly 22018 llyrest 22021 llyidm 22024 nllyidm 22025 cldllycmp 22031 txlly 22172 txnlly 22173 pthaus 22174 txhaus 22183 txkgen 22188 xkohaus 22189 xkococnlem 22195 cmetcaulem 23818 itg2add 24287 ulmdvlem3 24917 ax5seglem6 26647 fusgrfis 27039 wwlksnextfun 27603 umgr2wlkon 27656 connpconn 32379 cvmlift3lem2 32464 cvmlift3lem8 32470 noprefixmo 33099 nosupno 33100 scutbdaybnd 33172 ifscgr 33402 broutsideof3 33484 unblimceq0 33743 paddasslem10 36845 lhpexle2lem 37025 lhpexle3lem 37027 mpaaeu 39628 stoweidlem35 42197 stoweidlem56 42218 stoweidlem59 42221 |
Copyright terms: Public domain | W3C validator |