![]() |
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 1138 | . 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 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 cmetcaulem 24668 itg2add 25140 ulmdvlem3 25777 nosupprefixmo 27064 noinfprefixmo 27065 etasslt 27174 scutbdaybnd 27176 scutbdaybnd2 27177 addsproplem6 27308 negsproplem6 27353 ax5seglem6 27925 n4cyclfrgr 29277 connpconn 33869 cvmlift3lem2 33954 cvmlift3lem8 33960 broutsideof3 34740 unblimceq0 34999 paddasslem10 38321 lhpexle2lem 38501 lhpexle3lem 38503 stoweidlem35 44350 stoweidlem56 44371 stoweidlem59 44374 |
Copyright terms: Public domain | W3C validator |