![]() |
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 728 | 1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: poxp2 8080 sqrmo 15143 icodiamlt 15327 psgnunilem2 19284 haust1 22719 cnhaus 22721 isreg2 22744 llynlly 22844 restnlly 22849 llyrest 22852 llyidm 22855 nllyidm 22856 cldllycmp 22862 txlly 23003 txnlly 23004 pthaus 23005 txhaus 23014 txkgen 23019 xkohaus 23020 xkococnlem 23026 hauspwpwf1 23354 itg2add 25140 ulmdvlem3 25777 nosupno 27067 noinfno 27082 etasslt 27174 scutbdaybnd 27176 scutbdaybnd2 27177 addsproplem6 27308 negsproplem6 27353 ax5seglem6 27925 fusgrfis 28320 umgr2wlkon 28937 numclwwlk5 29374 connpconn 33869 cvmliftmolem2 33916 cvmlift2lem10 33946 cvmlift3lem2 33954 cvmlift3lem8 33960 broutsideof3 34740 unblimceq0 34999 paddasslem10 38321 lhpexle2lem 38501 lhpexle3lem 38503 cdlemj3 39315 cdlemkid4 39426 mpaaeu 41506 stoweidlem35 44350 stoweidlem56 44371 stoweidlem59 44374 |
Copyright terms: Public domain | W3C validator |