Theorem simp33l 1188

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

Assertion

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

Proof of Theorem simp33l

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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

This theorem is referenced by:  totprob  30489  cdleme19b  35592  cdleme19d  35594  cdleme19e  35595  cdleme20h  35604  cdleme20l2  35609  cdleme20m  35611  cdleme21d  35618  cdleme21e  35619  cdleme22e  35632  cdleme22f2  35635  cdleme22g  35636  cdleme26e  35647  cdleme28a  35658  cdleme28b  35659  cdleme37m  35750  cdleme39n  35754  cdlemeg46gfre  35820  cdlemg28a  35981  cdlemg28b  35991  cdlemk3  36121  cdlemk5a  36123  cdlemk6  36125  cdlemkuat  36154  cdlemkid2  36212