Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simprl3 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simprl3 | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl3 1059 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | |
2 | 1 | adantl 481 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: pwfseqlem5 9364 icodiamlt 14022 issubc3 16332 pgpfac1lem5 18301 clscon 21043 txlly 21249 txnlly 21250 itg2add 23332 ftc1a 23604 f1otrg 25551 ax5seglem6 25614 axcontlem10 25653 numclwwlk5 26639 locfinref 29236 btwnouttr2 31299 btwnconn1lem13 31376 midofsegid 31381 outsideofeq 31407 ivthALT 31500 mpaaeu 36739 dfsalgen2 39235 av-numclwwlk5 41542 |
Copyright terms: Public domain | W3C validator |