Theorem simp23l 1311

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ax5seglem6  29193  lshpkrlem5  39750  lplnexllnN  40200  4atexlemt  40689  4atex2  40713  4atex3  40717  trlval4  40824  cdlemc5  40831  cdlemc6  40832  cdlemd2  40835  cdleme0e  40853  cdleme0moN  40861  cdleme3g  40870  cdleme3h  40871  cdleme3  40873  cdleme4  40874  cdleme5  40876  cdleme9  40889  cdleme11fN  40900  cdleme11j  40903  cdleme11k  40904  cdleme11l  40905  cdleme11  40906  cdleme14  40909  cdleme15a  40910  cdleme15b  40911  cdleme15c  40912  cdleme16b  40915  cdleme16c  40916  cdleme16d  40917  cdleme16e  40918  cdleme16f  40919  cdleme17d1  40925  cdleme18c  40929  cdlemednpq  40935  cdleme19c  40941  cdleme20bN  40946  cdleme20d  40948  cdleme20f  40950  cdleme20g  40951  cdleme20h  40952  cdleme20j  40954  cdleme20l2  40957  cdleme20l  40958  cdleme20m  40959  cdleme22cN  40978  cdleme22d  40979  cdleme22e  40980  cdleme22f  40982  cdleme26fALTN  40998  cdleme26f  40999  cdleme26f2ALTN  41000  cdleme26f2  41001  cdleme27a  41003  cdleme28a  41006  cdlemefs44  41062  cdlemefs45ee  41066  cdleme32b  41078  cdleme32c  41079  cdleme32e  41081  cdleme35sn2aw  41094  cdleme37m  41098  cdleme39n  41102  cdleme40n  41104  cdleme40w  41106  cdleme42k  41120  cdlemeg47rv2  41146  cdlemeg46rjgN  41158  cdlemeg46rgv  41164  cdlemeg46req  41165  cdlemg2fv2  41236  cdlemg17h  41304  cdlemg31b0a  41331  cdlemg27b  41332  cdlemg31d  41336  cdlemg28b  41339  cdlemg28  41340  cdlemg29  41341  cdlemg33a  41342  cdlemg33b  41343  cdlemg33c  41344  cdlemg33d  41345  cdlemg33e  41346  cdlemg44a  41367  cdlemk7u-2N  41524  cdlemk11u-2N  41525  cdlemk12u-2N  41526  cdlemk26-3  41542  cdlemk27-3  41543  cdlemkfid3N  41561  cdlemn2  41831  cdlemn10  41842  cdlemn11c  41845