Theorem simp23r 1293

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

Assertion

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

Proof of Theorem simp23r

Step	Hyp	Ref	Expression
1		simp3r 1200	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1132	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ax5seglem6  28738  lshpkrlem5  38580  lplnexllnN  39031  4atexlemutvt  39521  cdlemc5  39662  cdlemd2  39666  cdleme0moN  39692  cdleme3h  39702  cdleme5  39707  cdleme9  39720  cdleme11l  39736  cdleme14  39740  cdleme15c  39743  cdleme16b  39746  cdleme16d  39748  cdleme16e  39749  cdlemednpq  39766  cdleme20bN  39777  cdleme20j  39785  cdleme20l2  39788  cdleme20l  39789  cdleme22cN  39809  cdleme22d  39810  cdleme22e  39811  cdleme22f  39813  cdleme26fALTN  39829  cdleme26f  39830  cdleme26f2ALTN  39831  cdleme26f2  39832  cdleme27a  39834  cdleme32b  39909  cdleme32d  39911  cdleme32f  39913  cdleme39n  39933  cdleme40n  39935  cdlemg2fv2  40067  cdlemg17h  40135  cdlemg27b  40163  cdlemg28b  40170  cdlemg28  40171  cdlemg29  40172  cdlemg33a  40173  cdlemg33d  40176  cdlemk7u-2N  40355  cdlemk11u-2N  40356  cdlemk12u-2N  40357  cdlemk26-3  40373  cdlemk27-3  40374  cdlemkfid3N  40392  cdlemn11c  40676

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »