Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simprl1 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simprl1 | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 1057 | . 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: pwfseqlem1 9359 pwfseqlem5 9364 icodiamlt 14022 issubc3 16332 pgpfac1lem5 18301 clscon 21043 txlly 21249 txnlly 21250 itg2add 23332 ftc1a 23604 f1otrg 25551 ax5seglem6 25614 axcontlem9 25652 axcontlem10 25653 extwwlkfablem2 26605 locfinref 29236 erdszelem7 30433 cvmlift2lem10 30548 btwnouttr2 31299 btwnconn1lem13 31376 broutsideof2 31399 mpaaeu 36739 dfsalgen2 39235 elwspths2spth 41171 digexp 42199 |
Copyright terms: Public domain | W3C validator |