Theorem simp23l 1287

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

Assertion

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

Proof of Theorem simp23l

Step	Hyp	Ref	Expression
1		simp3l 1194	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1127	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  ax5seglem6  26408  lshpkrlem5  35806  lplnexllnN  36256  4atexlemt  36745  4atex2  36769  4atex3  36773  trlval4  36880  cdlemc5  36887  cdlemc6  36888  cdlemd2  36891  cdleme0e  36909  cdleme0moN  36917  cdleme3g  36926  cdleme3h  36927  cdleme3  36929  cdleme4  36930  cdleme5  36932  cdleme9  36945  cdleme11fN  36956  cdleme11j  36959  cdleme11k  36960  cdleme11l  36961  cdleme11  36962  cdleme14  36965  cdleme15a  36966  cdleme15b  36967  cdleme15c  36968  cdleme16b  36971  cdleme16c  36972  cdleme16d  36973  cdleme16e  36974  cdleme16f  36975  cdleme17d1  36981  cdleme18c  36985  cdlemednpq  36991  cdleme19c  36997  cdleme20bN  37002  cdleme20d  37004  cdleme20f  37006  cdleme20g  37007  cdleme20h  37008  cdleme20j  37010  cdleme20l2  37013  cdleme20l  37014  cdleme20m  37015  cdleme22cN  37034  cdleme22d  37035  cdleme22e  37036  cdleme22f  37038  cdleme26fALTN  37054  cdleme26f  37055  cdleme26f2ALTN  37056  cdleme26f2  37057  cdleme27a  37059  cdleme28a  37062  cdlemefs44  37118  cdlemefs45ee  37122  cdleme32b  37134  cdleme32c  37135  cdleme32e  37137  cdleme35sn2aw  37150  cdleme37m  37154  cdleme39n  37158  cdleme40n  37160  cdleme40w  37162  cdleme42k  37176  cdlemeg47rv2  37202  cdlemeg46rjgN  37214  cdlemeg46rgv  37220  cdlemeg46req  37221  cdlemg2fv2  37292  cdlemg17h  37360  cdlemg31b0a  37387  cdlemg27b  37388  cdlemg31d  37392  cdlemg28b  37395  cdlemg28  37396  cdlemg29  37397  cdlemg33a  37398  cdlemg33b  37399  cdlemg33c  37400  cdlemg33d  37401  cdlemg33e  37402  cdlemg44a  37423  cdlemk7u-2N  37580  cdlemk11u-2N  37581  cdlemk12u-2N  37582  cdlemk26-3  37598  cdlemk27-3  37599  cdlemkfid3N  37617  cdlemn2  37887  cdlemn10  37898  cdlemn11c  37901