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 1129 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | ad2antrl 724 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: icodiamlt 14783 issubc3 17107 clsconn 21966 txlly 22172 txnlly 22173 itg2add 24287 ftc1a 24561 f1otrg 26584 ax5seglem6 26647 axcontlem9 26685 axcontlem10 26686 clwwlkf 27753 locfinref 31004 erdszelem7 32341 noprefixmo 33099 nosupbnd2 33113 btwnconn1lem13 33457 dfsalgen2 42501 |
Copyright terms: Public domain | W3C validator |