Theorem simp22l 1273

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1069

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 199  df-an 388  df-3an 1071

This theorem is referenced by:  ax5seglem6  26438  segconeu  33030  3atlem2  36102  lplncvrlvol2  36233  paddasslem15  36452  4atex  36694  trlval4  36806  cdlemc5  36813  cdlemc6  36814  cdlemd2  36817  cdlemd3  36818  cdlemd4  36819  cdleme0moN  36843  cdleme3g  36852  cdleme3h  36853  cdleme3  36855  cdleme11g  36883  cdleme11h  36884  cdleme11j  36885  cdleme11k  36886  cdleme11l  36887  cdleme11  36888  cdleme14  36891  cdleme15a  36892  cdleme15c  36894  cdleme15d  36895  cdleme15  36896  cdleme16b  36897  cdleme16c  36898  cdleme16d  36899  cdleme16e  36900  cdleme16f  36901  cdleme18a  36909  cdleme18b  36910  cdleme18c  36911  cdleme19b  36922  cdleme19e  36925  cdleme20bN  36928  cdleme20c  36929  cdleme20d  36930  cdleme20e  36931  cdleme20f  36932  cdleme20g  36933  cdleme20h  36934  cdleme20j  36936  cdleme20l2  36939  cdleme20l  36940  cdleme20m  36941  cdleme21ct  36947  cdleme22d  36961  cdleme22e  36962  cdleme22eALTN  36963  cdleme26e  36977  cdleme27a  36985  cdleme28a  36988  cdleme30a  36996  cdleme43fsv1snlem  37038  cdlemefs44  37044  cdlemefs45ee  37048  cdleme35sn2aw  37076  cdleme36a  37078  cdleme39n  37084  cdleme40m  37085  cdleme42k  37102  cdlemeg47rv2  37128  cdlemeg46frv  37143  cdlemeg46vrg  37145  cdlemeg46rgv  37146  cdlemeg46req  37147  cdlemg2fv2  37218  cdlemg4g  37234  cdlemg4  37235  cdlemg6c  37238  cdlemg8b  37246  cdlemg8c  37247  cdlemg9a  37250  cdlemg9b  37251  cdlemg9  37252  cdlemg12a  37261  cdlemg12b  37262  cdlemg12c  37263  cdlemg17h  37286  cdlemg18b  37297  cdlemg18c  37298  cdlemg31b0a  37313  cdlemg27b  37314  cdlemg31d  37318  cdlemg28b  37321  cdlemg33a  37324  cdlemg33b  37325  cdlemg33c  37326  cdlemg33d  37327  cdlemg33e  37328  cdlemg33  37329  cdlemh  37435  cdlemk6  37455  cdlemki  37459  cdlemksat  37464  cdlemksv2  37465  cdlemk7  37466  cdlemk11  37467  cdlemk12  37468  cdlemkole  37471  cdlemk14  37472  cdlemk15  37473  cdlemk17  37476  cdlemk1u  37477  cdlemk5u  37479  cdlemk6u  37480  cdlemk7u  37488  cdlemk11u  37489  cdlemk12u  37490  cdlemk7u-2N  37506  cdlemk11u-2N  37507  cdlemk12u-2N  37508  cdlemk20-2N  37510  cdlemk28-3  37526  cdlemk33N  37527  cdlemk34  37528  cdlemk37  37532  cdlemk39  37534  cdlemk35s  37555  cdlemk39s  37557  cdlemk47  37567  cdlemk48  37568  cdlemk50  37570  cdlemk51  37571  cdlemk52  37572  cdlemkyyN  37580  cdlemk43N  37581  cdlemn2  37813  cdlemn10  37824