![]() |
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 726 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ 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 396 df-3an 1086 |
This theorem is referenced by: poxp2 8126 icodiamlt 15385 psgnunilem2 19412 haust1 23206 cnhaus 23208 isreg2 23231 llynlly 23331 restnlly 23336 llyrest 23339 llyidm 23342 nllyidm 23343 cldllycmp 23349 txlly 23490 txnlly 23491 pthaus 23492 txhaus 23501 txkgen 23506 xkohaus 23507 xkococnlem 23513 cmetcaulem 25166 itg2add 25639 ulmdvlem3 26288 nosupprefixmo 27583 noinfprefixmo 27584 etasslt 27696 scutbdaybnd 27698 scutbdaybnd2 27699 addsproplem6 27841 negsproplem6 27895 mulsproplem13 27978 mulsproplem14 27979 mulsprop 27980 ax5seglem6 28695 n4cyclfrgr 30048 connpconn 34753 cvmlift3lem2 34838 cvmlift3lem8 34844 broutsideof3 35630 unblimceq0 35890 paddasslem10 39212 lhpexle2lem 39392 lhpexle3lem 39394 stoweidlem35 45305 stoweidlem56 45326 stoweidlem59 45329 |
Copyright terms: Public domain | W3C validator |