Theorem simp22l 1376

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 383  df-3an 1073

This theorem is referenced by:  ax5seglem6  26035  segconeu  32455  3atlem2  35292  lplncvrlvol2  35423  paddasslem15  35642  4atex  35884  trlval4  35997  cdlemc5  36004  cdlemc6  36005  cdlemd2  36008  cdlemd3  36009  cdlemd4  36010  cdleme0moN  36034  cdleme3g  36043  cdleme3h  36044  cdleme3  36046  cdleme11g  36074  cdleme11h  36075  cdleme11j  36076  cdleme11k  36077  cdleme11l  36078  cdleme11  36079  cdleme14  36082  cdleme15a  36083  cdleme15c  36085  cdleme15d  36086  cdleme15  36087  cdleme16b  36088  cdleme16c  36089  cdleme16d  36090  cdleme16e  36091  cdleme16f  36092  cdleme18a  36100  cdleme18b  36101  cdleme18c  36102  cdleme19b  36113  cdleme19e  36116  cdleme20bN  36119  cdleme20c  36120  cdleme20d  36121  cdleme20e  36122  cdleme20f  36123  cdleme20g  36124  cdleme20h  36125  cdleme20j  36127  cdleme20l2  36130  cdleme20l  36131  cdleme20m  36132  cdleme21ct  36138  cdleme22d  36152  cdleme22e  36153  cdleme22eALTN  36154  cdleme26e  36168  cdleme27a  36176  cdleme28a  36179  cdleme30a  36187  cdleme43fsv1snlem  36229  cdlemefs44  36235  cdlemefs45ee  36239  cdleme35sn2aw  36267  cdleme36a  36269  cdleme39n  36275  cdleme40m  36276  cdleme42k  36293  cdlemeg47rv2  36319  cdlemeg46frv  36334  cdlemeg46vrg  36336  cdlemeg46rgv  36337  cdlemeg46req  36338  cdlemg2fv2  36409  cdlemg4g  36425  cdlemg4  36426  cdlemg6c  36429  cdlemg8b  36437  cdlemg8c  36438  cdlemg9a  36441  cdlemg9b  36442  cdlemg9  36443  cdlemg12a  36452  cdlemg12b  36453  cdlemg12c  36454  cdlemg17h  36477  cdlemg18b  36488  cdlemg18c  36489  cdlemg31b0a  36504  cdlemg27b  36505  cdlemg31d  36509  cdlemg28b  36512  cdlemg33a  36515  cdlemg33b  36516  cdlemg33c  36517  cdlemg33d  36518  cdlemg33e  36519  cdlemg33  36520  cdlemh  36626  cdlemk6  36646  cdlemki  36650  cdlemksat  36655  cdlemksv2  36656  cdlemk7  36657  cdlemk11  36658  cdlemk12  36659  cdlemkole  36662  cdlemk14  36663  cdlemk15  36664  cdlemk17  36667  cdlemk1u  36668  cdlemk5u  36670  cdlemk6u  36671  cdlemk7u  36679  cdlemk11u  36680  cdlemk12u  36681  cdlemk7u-2N  36697  cdlemk11u-2N  36698  cdlemk12u-2N  36699  cdlemk20-2N  36701  cdlemk28-3  36717  cdlemk33N  36718  cdlemk34  36719  cdlemk37  36723  cdlemk39  36725  cdlemk35s  36746  cdlemk39s  36748  cdlemk47  36758  cdlemk48  36759  cdlemk50  36761  cdlemk51  36762  cdlemk52  36763  cdlemkyyN  36771  cdlemk43N  36772  cdlemn2  37005  cdlemn10  37016