![]() |
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 8123 icodiamlt 15379 psgnunilem2 19405 haust1 23178 cnhaus 23180 isreg2 23203 llynlly 23303 restnlly 23308 llyrest 23311 llyidm 23314 nllyidm 23315 cldllycmp 23321 txlly 23462 txnlly 23463 pthaus 23464 txhaus 23473 txkgen 23478 xkohaus 23479 xkococnlem 23485 cmetcaulem 25138 itg2add 25611 ulmdvlem3 26255 nosupprefixmo 27549 noinfprefixmo 27550 etasslt 27662 scutbdaybnd 27664 scutbdaybnd2 27665 addsproplem6 27807 negsproplem6 27861 mulsproplem13 27944 mulsproplem14 27945 mulsprop 27946 ax5seglem6 28661 n4cyclfrgr 30013 connpconn 34715 cvmlift3lem2 34800 cvmlift3lem8 34806 broutsideof3 35593 unblimceq0 35873 paddasslem10 39190 lhpexle2lem 39370 lhpexle3lem 39372 stoweidlem35 45236 stoweidlem56 45257 stoweidlem59 45260 |
Copyright terms: Public domain | W3C validator |