Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simprr2 | 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 |
---|---|
simprr2 | ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 1133 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | ad2antll 727 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: icodiamlt 14789 psgnunilem2 18617 haust1 21954 cnhaus 21956 isreg2 21979 llynlly 22079 restnlly 22084 llyrest 22087 llyidm 22090 nllyidm 22091 cldllycmp 22097 txlly 22238 txnlly 22239 pthaus 22240 txhaus 22249 txkgen 22254 xkohaus 22255 xkococnlem 22261 cmetcaulem 23885 itg2add 24354 ulmdvlem3 24984 ax5seglem6 26714 n4cyclfrgr 28064 connpconn 32477 cvmlift3lem2 32562 cvmlift3lem8 32568 noprefixmo 33197 scutbdaybnd 33270 broutsideof3 33582 unblimceq0 33841 paddasslem10 36959 lhpexle2lem 37139 lhpexle3lem 37141 stoweidlem35 42313 stoweidlem56 42334 stoweidlem59 42337 |
Copyright terms: Public domain | W3C validator |