Theorem simp22l 1294

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

Assertion

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

Proof of Theorem simp22l

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

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

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 1089

This theorem is referenced by:  ttrclselem2  9647  ax5seglem6  29003  segconeu  36193  3atlem2  39930  lplncvrlvol2  40061  paddasslem15  40280  4atex  40522  trlval4  40634  cdlemc5  40641  cdlemc6  40642  cdlemd2  40645  cdlemd3  40646  cdlemd4  40647  cdleme0moN  40671  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme11g  40711  cdleme11h  40712  cdleme11j  40713  cdleme11k  40714  cdleme11l  40715  cdleme11  40716  cdleme14  40719  cdleme15a  40720  cdleme15c  40722  cdleme15d  40723  cdleme15  40724  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme18a  40737  cdleme18b  40738  cdleme18c  40739  cdleme19b  40750  cdleme19e  40753  cdleme20bN  40756  cdleme20c  40757  cdleme20d  40758  cdleme20e  40759  cdleme20f  40760  cdleme20g  40761  cdleme20h  40762  cdleme20j  40764  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21ct  40775  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme26e  40805  cdleme27a  40813  cdleme28a  40816  cdleme30a  40824  cdleme43fsv1snlem  40866  cdlemefs44  40872  cdlemefs45ee  40876  cdleme35sn2aw  40904  cdleme36a  40906  cdleme39n  40912  cdleme40m  40913  cdleme42k  40930  cdlemeg47rv2  40956  cdlemeg46frv  40971  cdlemeg46vrg  40973  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemg2fv2  41046  cdlemg4g  41062  cdlemg4  41063  cdlemg6c  41066  cdlemg8b  41074  cdlemg8c  41075  cdlemg9a  41078  cdlemg9b  41079  cdlemg9  41080  cdlemg12a  41089  cdlemg12b  41090  cdlemg12c  41091  cdlemg17h  41114  cdlemg18b  41125  cdlemg18c  41126  cdlemg31b0a  41141  cdlemg27b  41142  cdlemg31d  41146  cdlemg28b  41149  cdlemg33a  41152  cdlemg33b  41153  cdlemg33c  41154  cdlemg33d  41155  cdlemg33e  41156  cdlemg33  41157  cdlemh  41263  cdlemk6  41283  cdlemki  41287  cdlemksat  41292  cdlemksv2  41293  cdlemk7  41294  cdlemk11  41295  cdlemk12  41296  cdlemkole  41299  cdlemk14  41300  cdlemk15  41301  cdlemk17  41304  cdlemk1u  41305  cdlemk5u  41307  cdlemk6u  41308  cdlemk7u  41316  cdlemk11u  41317  cdlemk12u  41318  cdlemk7u-2N  41334  cdlemk11u-2N  41335  cdlemk12u-2N  41336  cdlemk20-2N  41338  cdlemk28-3  41354  cdlemk33N  41355  cdlemk34  41356  cdlemk37  41360  cdlemk39  41362  cdlemk35s  41383  cdlemk39s  41385  cdlemk47  41395  cdlemk48  41396  cdlemk50  41398  cdlemk51  41399  cdlemk52  41400  cdlemkyyN  41408  cdlemk43N  41409  cdlemn2  41641  cdlemn10  41652