![]() |
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.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
Ref | Expression |
---|---|
simprl3 | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 1139 | . 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: poxp3 8136 ttrcltr 9711 pwfseqlem5 10658 icodiamlt 15382 issubc3 17799 pgpfac1lem5 19949 clsconn 22934 txlly 23140 txnlly 23141 itg2add 25277 ftc1a 25554 nosupprefixmo 27203 noinfprefixmo 27204 nosupbnd2 27219 noinfbnd2 27234 mulsprop 27586 f1otrg 28122 ax5seglem6 28192 axcontlem10 28231 numclwwlk5 29641 locfinref 32821 btwnouttr2 34994 btwnconn1lem13 35071 midofsegid 35076 outsideofeq 35102 ivthALT 35220 mpaaeu 41892 dfsalgen2 45057 |
Copyright terms: Public domain | W3C validator |