simp23l - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > simp23l		Structured version Visualization version GIF version

Theorem simp23l 1292

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

**Assertion**
Ref	Expression
simp23l	⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑)

**Proof of Theorem simp23l**
Step	Hyp	Ref	Expression
1		simp3l 1199	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1132	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085

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 396 df-3an 1087

This theorem is referenced by: ax5seglem6 28738 lshpkrlem5 38580 lplnexllnN 39031 4atexlemt 39520 4atex2 39544 4atex3 39548 trlval4 39655 cdlemc5 39662 cdlemc6 39663 cdlemd2 39666 cdleme0e 39684 cdleme0moN 39692 cdleme3g 39701 cdleme3h 39702 cdleme3 39704 cdleme4 39705 cdleme5 39707 cdleme9 39720 cdleme11fN 39731 cdleme11j 39734 cdleme11k 39735 cdleme11l 39736 cdleme11 39737 cdleme14 39740 cdleme15a 39741 cdleme15b 39742 cdleme15c 39743 cdleme16b 39746 cdleme16c 39747 cdleme16d 39748 cdleme16e 39749 cdleme16f 39750 cdleme17d1 39756 cdleme18c 39760 cdlemednpq 39766 cdleme19c 39772 cdleme20bN 39777 cdleme20d 39779 cdleme20f 39781 cdleme20g 39782 cdleme20h 39783 cdleme20j 39785 cdleme20l2 39788 cdleme20l 39789 cdleme20m 39790 cdleme22cN 39809 cdleme22d 39810 cdleme22e 39811 cdleme22f 39813 cdleme26fALTN 39829 cdleme26f 39830 cdleme26f2ALTN 39831 cdleme26f2 39832 cdleme27a 39834 cdleme28a 39837 cdlemefs44 39893 cdlemefs45ee 39897 cdleme32b 39909 cdleme32c 39910 cdleme32e 39912 cdleme35sn2aw 39925 cdleme37m 39929 cdleme39n 39933 cdleme40n 39935 cdleme40w 39937 cdleme42k 39951 cdlemeg47rv2 39977 cdlemeg46rjgN 39989 cdlemeg46rgv 39995 cdlemeg46req 39996 cdlemg2fv2 40067 cdlemg17h 40135 cdlemg31b0a 40162 cdlemg27b 40163 cdlemg31d 40167 cdlemg28b 40170 cdlemg28 40171 cdlemg29 40172 cdlemg33a 40173 cdlemg33b 40174 cdlemg33c 40175 cdlemg33d 40176 cdlemg33e 40177 cdlemg44a 40198 cdlemk7u-2N 40355 cdlemk11u-2N 40356 cdlemk12u-2N 40357 cdlemk26-3 40373 cdlemk27-3 40374 cdlemkfid3N 40392 cdlemn2 40662 cdlemn10 40673 cdlemn11c 40676

W3C validator

	
		OSZAR »