Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpl3r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl3r | ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3r 1083 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | adantr 480 | 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: tfisi 6950 omopth2 7551 ltmul1a 10751 xmulasslem3 11988 xadddi2 11999 swrdsbslen 13300 swrdspsleq 13301 dvdsadd2b 14866 pockthg 15448 psgnunilem4 17740 efgred 17984 marrepeval 20188 submaeval 20207 mdetmul 20248 minmar1eval 20274 ptbasin 21190 basqtop 21324 xrsmopn 22423 axpasch 25621 axeuclid 25643 extwwlkfablem2 26605 br4 30901 btwnouttr2 31299 trisegint 31305 cgrxfr 31332 lineext 31353 btwnconn1lem13 31376 btwnconn1lem14 31377 btwnconn3 31380 brsegle 31385 brsegle2 31386 segleantisym 31392 outsideofeu 31408 lineunray 31424 lineelsb2 31425 cvrcmp 33588 atcvrj2b 33736 3dimlem3 33765 3dimlem3OLDN 33766 3dim3 33773 ps-1 33781 ps-2 33782 lplnnle2at 33845 2llnm3N 33873 4atlem0a 33897 4atlem3 33900 4atlem3a 33901 lnatexN 34083 paddasslem8 34131 paddasslem9 34132 paddasslem10 34133 paddasslem12 34135 paddasslem13 34136 lhpexle2lem 34313 lhpexle3 34316 lhpat3 34350 4atex 34380 trlval2 34468 trlval4 34493 cdleme16 34590 cdleme21 34643 cdleme21k 34644 cdleme27cl 34672 cdleme27N 34675 cdleme43fsv1snlem 34726 cdleme48fvg 34806 cdlemg8 34937 cdlemg15a 34961 cdlemg16z 34965 cdlemg24 34994 cdlemg38 35021 cdlemg40 35023 trlcone 35034 cdlemj2 35128 tendoid0 35131 tendoconid 35135 cdlemk34 35216 cdlemk38 35221 cdlemkid4 35240 cdlemk53 35263 tendospcanN 35330 dihvalcqpre 35542 dihmeetlem15N 35628 qirropth 36491 mzpcong 36557 jm2.26 36587 aomclem6 36647 islptre 38686 limccog 38687 limcleqr 38711 fourierdlem42 39042 elaa2 39127 |
Copyright terms: Public domain | W3C validator |