Theorem simp22l 1311

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

Assertion

Ref	Expression
simp22l	⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)

Proof of Theorem simp22l

Step	Hyp	Ref	Expression
1		simp2l 1218	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 1152	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ttrclselem2  9696  ax5seglem6  29265  segconeu  36484  3atlem2  40239  lplncvrlvol2  40370  paddasslem15  40589  4atex  40831  trlval4  40943  cdlemc5  40950  cdlemc6  40951  cdlemd2  40954  cdlemd3  40955  cdlemd4  40956  cdleme0moN  40980  cdleme3g  40989  cdleme3h  40990  cdleme3  40992  cdleme11g  41020  cdleme11h  41021  cdleme11j  41022  cdleme11k  41023  cdleme11l  41024  cdleme11  41025  cdleme14  41028  cdleme15a  41029  cdleme15c  41031  cdleme15d  41032  cdleme15  41033  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme16f  41038  cdleme18a  41046  cdleme18b  41047  cdleme18c  41048  cdleme19b  41059  cdleme19e  41062  cdleme20bN  41065  cdleme20c  41066  cdleme20d  41067  cdleme20e  41068  cdleme20f  41069  cdleme20g  41070  cdleme20h  41071  cdleme20j  41073  cdleme20l2  41076  cdleme20l  41077  cdleme20m  41078  cdleme21ct  41084  cdleme22d  41098  cdleme22e  41099  cdleme22eALTN  41100  cdleme26e  41114  cdleme27a  41122  cdleme28a  41125  cdleme30a  41133  cdleme43fsv1snlem  41175  cdlemefs44  41181  cdlemefs45ee  41185  cdleme35sn2aw  41213  cdleme36a  41215  cdleme39n  41221  cdleme40m  41222  cdleme42k  41239  cdlemeg47rv2  41265  cdlemeg46frv  41280  cdlemeg46vrg  41282  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemg2fv2  41355  cdlemg4g  41371  cdlemg4  41372  cdlemg6c  41375  cdlemg8b  41383  cdlemg8c  41384  cdlemg9a  41387  cdlemg9b  41388  cdlemg9  41389  cdlemg12a  41398  cdlemg12b  41399  cdlemg12c  41400  cdlemg17h  41423  cdlemg18b  41434  cdlemg18c  41435  cdlemg31b0a  41450  cdlemg27b  41451  cdlemg31d  41455  cdlemg28b  41458  cdlemg33a  41461  cdlemg33b  41462  cdlemg33c  41463  cdlemg33d  41464  cdlemg33e  41465  cdlemg33  41466  cdlemh  41572  cdlemk6  41592  cdlemki  41596  cdlemksat  41601  cdlemksv2  41602  cdlemk7  41603  cdlemk11  41604  cdlemk12  41605  cdlemkole  41608  cdlemk14  41609  cdlemk15  41610  cdlemk17  41613  cdlemk1u  41614  cdlemk5u  41616  cdlemk6u  41617  cdlemk7u  41625  cdlemk11u  41626  cdlemk12u  41627  cdlemk7u-2N  41643  cdlemk11u-2N  41644  cdlemk12u-2N  41645  cdlemk20-2N  41647  cdlemk28-3  41663  cdlemk33N  41664  cdlemk34  41665  cdlemk37  41669  cdlemk39  41671  cdlemk35s  41692  cdlemk39s  41694  cdlemk47  41704  cdlemk48  41705  cdlemk50  41707  cdlemk51  41708  cdlemk52  41709  cdlemkyyN  41717  cdlemk43N  41718  cdlemn2  41950  cdlemn10  41961