Theorem simp31r 1293

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

Assertion

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

Proof of Theorem simp31r

Step	Hyp	Ref	Expression
1		simp1r 1194	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant3 1131	1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ps-2c  36679  cdlema1N  36942  cdlemednpq  37450  cdleme19e  37458  cdleme20h  37467  cdleme20j  37469  cdleme20l2  37472  cdleme20m  37474  cdleme22a  37491  cdleme22cN  37493  cdleme22f2  37498  cdleme26f2ALTN  37515  cdleme37m  37613  cdlemg12f  37799  cdlemg12g  37800  cdlemg12  37801  cdlemg28a  37844  cdlemg29  37856  cdlemg33a  37857  cdlemg36  37865  cdlemk16a  38007  cdlemk21-2N  38042  cdlemk54  38109  dihord10  38374