![]() |
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 1137 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | ad2antrl 728 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 207 df-an 396 df-3an 1088 |
This theorem is referenced by: poxp3 8174 ttrcltr 9754 pwfseqlem5 10701 icodiamlt 15471 issubc3 17900 pgpfac1lem5 20114 clsconn 23454 txlly 23660 txnlly 23661 itg2add 25809 ftc1a 26093 nosupprefixmo 27760 noinfprefixmo 27761 nosupbnd2 27776 noinfbnd2 27791 mulsprop 28171 f1otrg 28894 ax5seglem6 28964 axcontlem10 29003 numclwwlk5 30417 locfinref 33802 btwnouttr2 36004 btwnconn1lem13 36081 midofsegid 36086 outsideofeq 36112 ivthALT 36318 mpaaeu 43139 dfsalgen2 46297 grtrimap 47851 |
Copyright terms: Public domain | W3C validator |