Theorem simp22l 1293

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

Assertion

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

Proof of Theorem simp22l

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

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

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 1088

This theorem is referenced by:  ttrclselem2  9623  ax5seglem6  28914  segconeu  36076  3atlem2  39603  lplncvrlvol2  39734  paddasslem15  39953  4atex  40195  trlval4  40307  cdlemc5  40314  cdlemc6  40315  cdlemd2  40318  cdlemd3  40319  cdlemd4  40320  cdleme0moN  40344  cdleme3g  40353  cdleme3h  40354  cdleme3  40356  cdleme11g  40384  cdleme11h  40385  cdleme11j  40386  cdleme11k  40387  cdleme11l  40388  cdleme11  40389  cdleme14  40392  cdleme15a  40393  cdleme15c  40395  cdleme15d  40396  cdleme15  40397  cdleme16b  40398  cdleme16c  40399  cdleme16d  40400  cdleme16e  40401  cdleme16f  40402  cdleme18a  40410  cdleme18b  40411  cdleme18c  40412  cdleme19b  40423  cdleme19e  40426  cdleme20bN  40429  cdleme20c  40430  cdleme20d  40431  cdleme20e  40432  cdleme20f  40433  cdleme20g  40434  cdleme20h  40435  cdleme20j  40437  cdleme20l2  40440  cdleme20l  40441  cdleme20m  40442  cdleme21ct  40448  cdleme22d  40462  cdleme22e  40463  cdleme22eALTN  40464  cdleme26e  40478  cdleme27a  40486  cdleme28a  40489  cdleme30a  40497  cdleme43fsv1snlem  40539  cdlemefs44  40545  cdlemefs45ee  40549  cdleme35sn2aw  40577  cdleme36a  40579  cdleme39n  40585  cdleme40m  40586  cdleme42k  40603  cdlemeg47rv2  40629  cdlemeg46frv  40644  cdlemeg46vrg  40646  cdlemeg46rgv  40647  cdlemeg46req  40648  cdlemg2fv2  40719  cdlemg4g  40735  cdlemg4  40736  cdlemg6c  40739  cdlemg8b  40747  cdlemg8c  40748  cdlemg9a  40751  cdlemg9b  40752  cdlemg9  40753  cdlemg12a  40762  cdlemg12b  40763  cdlemg12c  40764  cdlemg17h  40787  cdlemg18b  40798  cdlemg18c  40799  cdlemg31b0a  40814  cdlemg27b  40815  cdlemg31d  40819  cdlemg28b  40822  cdlemg33a  40825  cdlemg33b  40826  cdlemg33c  40827  cdlemg33d  40828  cdlemg33e  40829  cdlemg33  40830  cdlemh  40936  cdlemk6  40956  cdlemki  40960  cdlemksat  40965  cdlemksv2  40966  cdlemk7  40967  cdlemk11  40968  cdlemk12  40969  cdlemkole  40972  cdlemk14  40973  cdlemk15  40974  cdlemk17  40977  cdlemk1u  40978  cdlemk5u  40980  cdlemk6u  40981  cdlemk7u  40989  cdlemk11u  40990  cdlemk12u  40991  cdlemk7u-2N  41007  cdlemk11u-2N  41008  cdlemk12u-2N  41009  cdlemk20-2N  41011  cdlemk28-3  41027  cdlemk33N  41028  cdlemk34  41029  cdlemk37  41033  cdlemk39  41035  cdlemk35s  41056  cdlemk39s  41058  cdlemk47  41068  cdlemk48  41069  cdlemk50  41071  cdlemk51  41072  cdlemk52  41073  cdlemkyyN  41081  cdlemk43N  41082  cdlemn2  41314  cdlemn10  41325