![]() |
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 1130 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antll 700 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 |
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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: sqrmo 14199 icodiamlt 14381 psgnunilem2 18121 haust1 21376 cnhaus 21378 isreg2 21401 llynlly 21500 restnlly 21505 llyrest 21508 llyidm 21511 nllyidm 21512 cldllycmp 21518 txlly 21659 txnlly 21660 pthaus 21661 txhaus 21670 txkgen 21675 xkohaus 21676 xkococnlem 21682 hauspwpwf1 22010 itg2add 23745 ulmdvlem3 24375 ax5seglem6 26034 fusgrfis 26444 umgr2wlkon 27096 numclwwlk5 27584 connpconn 31552 cvmliftmolem2 31599 cvmlift2lem10 31629 cvmlift3lem2 31637 cvmlift3lem8 31643 nosupno 32183 scutbdaybnd 32255 broutsideof3 32567 unblimceq0 32832 paddasslem10 35633 lhpexle2lem 35813 lhpexle3lem 35815 cdlemj3 36628 cdlemkid4 36739 mpaaeu 38242 stoweidlem35 40765 stoweidlem56 40786 stoweidlem59 40789 |
Copyright terms: Public domain | W3C validator |