Theorem simp33l 1400

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

Assertion

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

Proof of Theorem simp33l

Step	Hyp	Ref	Expression
1		simp3l 1259	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant3 1166	1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108

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 386  df-3an 1110

This theorem is referenced by:  totprob  30998  cdleme19b  36317  cdleme19d  36319  cdleme19e  36320  cdleme20h  36329  cdleme20l2  36334  cdleme20m  36336  cdleme21d  36343  cdleme21e  36344  cdleme22e  36357  cdleme22f2  36360  cdleme22g  36361  cdleme26e  36372  cdleme28a  36383  cdleme28b  36384  cdleme37m  36475  cdleme39n  36479  cdlemeg46gfre  36545  cdlemg28a  36706  cdlemg28b  36716  cdlemk3  36846  cdlemk5a  36848  cdlemk6  36850  cdlemkuat  36879  cdlemkid2  36937