![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simprl2 | 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 |
---|---|
simprl2 | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 1138 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | ad2antrl 727 | 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 8124 poxp3 8131 icodiamlt 15378 issubc3 17795 clsconn 22916 txlly 23122 txnlly 23123 itg2add 25259 ftc1a 25536 nosupprefixmo 27183 noinfprefixmo 27184 nosupbnd2 27199 noinfbnd2 27214 mulsprop 27566 f1otrg 28102 ax5seglem6 28172 axcontlem9 28210 axcontlem10 28211 clwwlkf 29280 locfinref 32759 erdszelem7 34126 btwnconn1lem13 35009 dfsalgen2 44992 |
Copyright terms: Public domain | W3C validator |