![]() |
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 1138 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | ad2antrl 726 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 397 df-3an 1089 |
This theorem is referenced by: poxp3 8138 ttrcltr 9713 pwfseqlem5 10660 icodiamlt 15386 issubc3 17803 pgpfac1lem5 19990 clsconn 23154 txlly 23360 txnlly 23361 itg2add 25501 ftc1a 25778 nosupprefixmo 27427 noinfprefixmo 27428 nosupbnd2 27443 noinfbnd2 27458 mulsprop 27813 f1otrg 28377 ax5seglem6 28447 axcontlem10 28486 numclwwlk5 29896 locfinref 33107 btwnouttr2 35286 btwnconn1lem13 35363 midofsegid 35368 outsideofeq 35394 ivthALT 35523 mpaaeu 42194 dfsalgen2 45356 |
Copyright terms: Public domain | W3C validator |