simpl21 - Metamath Proof Explorer

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

Theorem simpl21 1249

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

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

**Proof of Theorem simpl21**
Step	Hyp	Ref	Expression
1		simpl1 1189	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl2 1184	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: frrlem10 8294 nosupbnd2lem1 27641 noinfbnd2lem1 27656 brbtwn2 28709 ax5seglem3a 28734 ax5seg 28742 axpasch 28745 axeuclid 28767 br8d 32393 br8 35344 cgrextend 35598 segconeq 35600 trisegint 35618 ifscgr 35634 cgrsub 35635 cgrxfr 35645 lineext 35666 seglecgr12im 35700 segletr 35704 lineunray 35737 lineelsb2 35738 cvrcmp 38749 cvlatexch3 38804 cvlsupr2 38809 atexchcvrN 38907 3dim1 38934 3dim2 38935 ps-1 38944 ps-2 38945 3atlem3 38952 3atlem5 38954 lplnnle2at 39008 lplnllnneN 39023 2llnjaN 39033 4atlem3 39063 4atlem10b 39072 4atlem12 39079 2llnma3r 39255 paddasslem4 39290 paddasslem7 39293 paddasslem8 39294 paddasslem12 39298 paddasslem13 39299 pmodlem1 39313 pmodlem2 39314 llnexchb2lem 39335 4atex2 39544 ltrnatlw 39650 trlval4 39655 arglem1N 39657 cdlemd4 39668 cdlemd5 39669 cdleme0moN 39692 cdleme16 39752 cdleme20 39791 cdleme21j 39803 cdleme21k 39805 cdleme27N 39836 cdleme28c 39839 cdleme43fsv1snlem 39887 cdleme38n 39931 cdleme40n 39935 cdleme41snaw 39943 cdlemg6c 40087 cdlemg8c 40096 cdlemg8 40098 cdlemg12e 40114 cdlemg16 40124 cdlemg16ALTN 40125 cdlemg16z 40126 cdlemg16zz 40127 cdlemg18a 40145 cdlemg20 40152 cdlemg22 40154 cdlemg37 40156 cdlemg27b 40163 cdlemg31d 40167 cdlemg33 40178 cdlemg38 40182 cdlemg44b 40199 cdlemk38 40382 cdlemk35s-id 40405 cdlemk39s-id 40407 cdlemk55 40428 cdlemk35u 40431 cdlemk55u 40433 cdleml3N 40445 cdlemn11pre 40677

	
		OSZAR »