| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simprr1 | 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 |
|---|---|
| simprr1 | ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp1 1137 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
| 2 | 1 | ad2antll 729 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: poxp2 8168 sqrmo 15290 icodiamlt 15474 psgnunilem2 19513 haust1 23360 cnhaus 23362 isreg2 23385 llynlly 23485 restnlly 23490 llyrest 23493 llyidm 23496 nllyidm 23497 cldllycmp 23503 txlly 23644 txnlly 23645 pthaus 23646 txhaus 23655 txkgen 23660 xkohaus 23661 xkococnlem 23667 hauspwpwf1 23995 itg2add 25794 ulmdvlem3 26445 nosupno 27748 noinfno 27763 etasslt 27858 scutbdaybnd 27860 scutbdaybnd2 27861 addsproplem6 28007 negsproplem6 28065 mulsproplem13 28154 mulsproplem14 28155 mulsprop 28156 ax5seglem6 28949 fusgrfis 29347 umgr2wlkon 29970 numclwwlk5 30407 connpconn 35240 cvmliftmolem2 35287 cvmlift2lem10 35317 cvmlift3lem2 35325 cvmlift3lem8 35331 broutsideof3 36127 unblimceq0 36508 paddasslem10 39831 lhpexle2lem 40011 lhpexle3lem 40013 cdlemj3 40825 cdlemkid4 40936 mpaaeu 43162 stoweidlem35 46050 stoweidlem56 46071 stoweidlem59 46074 |
| Copyright terms: Public domain | W3C validator |