![]() |
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 1134 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | ad2antll 727 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: poxp2 8154 icodiamlt 15422 psgnunilem2 19457 haust1 23276 cnhaus 23278 isreg2 23301 llynlly 23401 restnlly 23406 llyrest 23409 llyidm 23412 nllyidm 23413 cldllycmp 23419 txlly 23560 txnlly 23561 pthaus 23562 txhaus 23571 txkgen 23576 xkohaus 23577 xkococnlem 23583 cmetcaulem 25236 itg2add 25709 ulmdvlem3 26358 nosupprefixmo 27653 noinfprefixmo 27654 etasslt 27766 scutbdaybnd 27768 scutbdaybnd2 27769 addsproplem6 27911 negsproplem6 27965 mulsproplem13 28048 mulsproplem14 28049 mulsprop 28050 ax5seglem6 28765 n4cyclfrgr 30121 connpconn 34878 cvmlift3lem2 34963 cvmlift3lem8 34969 broutsideof3 35755 unblimceq0 36015 paddasslem10 39334 lhpexle2lem 39514 lhpexle3lem 39516 stoweidlem35 45452 stoweidlem56 45473 stoweidlem59 45476 |
Copyright terms: Public domain | W3C validator |