Theorem simp22l 1180

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ax5seglem6  25814  segconeu  32118  3atlem2  34770  lplncvrlvol2  34901  paddasslem15  35120  4atex  35362  trlval4  35475  cdlemc5  35482  cdlemc6  35483  cdlemd2  35486  cdlemd3  35487  cdlemd4  35488  cdleme0moN  35512  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme11g  35552  cdleme11h  35553  cdleme11j  35554  cdleme11k  35555  cdleme11l  35556  cdleme11  35557  cdleme14  35560  cdleme15a  35561  cdleme15c  35563  cdleme15d  35564  cdleme15  35565  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme18a  35578  cdleme18b  35579  cdleme18c  35580  cdleme19b  35592  cdleme19e  35595  cdleme20bN  35598  cdleme20c  35599  cdleme20d  35600  cdleme20e  35601  cdleme20f  35602  cdleme20g  35603  cdleme20h  35604  cdleme20j  35606  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21ct  35617  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme26e  35647  cdleme27a  35655  cdleme28a  35658  cdleme30a  35666  cdleme43fsv1snlem  35708  cdlemefs44  35714  cdlemefs45ee  35718  cdleme35sn2aw  35746  cdleme36a  35748  cdleme39n  35754  cdleme40m  35755  cdleme42k  35772  cdlemeg47rv2  35798  cdlemeg46frv  35813  cdlemeg46vrg  35815  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemg2fv2  35888  cdlemg4g  35904  cdlemg4  35905  cdlemg6c  35908  cdlemg8b  35916  cdlemg8c  35917  cdlemg9a  35920  cdlemg9b  35921  cdlemg9  35922  cdlemg12a  35931  cdlemg12b  35932  cdlemg12c  35933  cdlemg17h  35956  cdlemg18b  35967  cdlemg18c  35968  cdlemg31b0a  35983  cdlemg27b  35984  cdlemg31d  35988  cdlemg28b  35991  cdlemg33a  35994  cdlemg33b  35995  cdlemg33c  35996  cdlemg33d  35997  cdlemg33e  35998  cdlemg33  35999  cdlemh  36105  cdlemk6  36125  cdlemki  36129  cdlemksat  36134  cdlemksv2  36135  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk17  36146  cdlemk1u  36147  cdlemk5u  36149  cdlemk6u  36150  cdlemk7u  36158  cdlemk11u  36159  cdlemk12u  36160  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk12u-2N  36178  cdlemk20-2N  36180  cdlemk28-3  36196  cdlemk33N  36197  cdlemk34  36198  cdlemk37  36202  cdlemk39  36204  cdlemk35s  36225  cdlemk39s  36227  cdlemk47  36237  cdlemk48  36238  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemkyyN  36250  cdlemk43N  36251  cdlemn2  36484  cdlemn10  36495