Theorem simp2ll 1236

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

Assertion

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

Proof of Theorem simp2ll

Step	Hyp	Ref	Expression
1		simpll 765	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant2 1130	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:  tfrlem5  8016  omeu  8211  expmordi  13532  4sqlem18  16298  vdwlem10  16326  0catg  16958  mvrf1  20205  mdetuni0  21230  mdetmul  21232  tsmsxp  22763  ax5seglem3  26717  btwnconn1lem1  33548  btwnconn1lem2  33549  btwnconn1lem3  33550  btwnconn1lem12  33559  btwnconn1lem13  33560  lshpkrlem6  36266  athgt  36607  2llnjN  36718  dalaw  37037  lhpmcvr4N  37177  cdlemb2  37192  4atexlemex6  37225  cdlemd7  37355  cdleme01N  37372  cdleme02N  37373  cdleme0ex1N  37374  cdleme0ex2N  37375  cdleme7aa  37393  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme7ga  37399  cdleme7  37400  cdleme11a  37411  cdleme20k  37470  cdleme27cl  37517  cdleme42e  37630  cdleme42h  37633  cdleme42i  37634  cdlemf  37714  cdlemg2kq  37753  cdlemg2m  37755  cdlemg8a  37778  cdlemg11aq  37789  cdlemg10c  37790  cdlemg11b  37793  cdlemg17a  37812  cdlemg31b0N  37845  cdlemg31c  37850  cdlemg33c0  37853  cdlemg41  37869  cdlemh2  37967  cdlemn9  38356  dihglbcpreN  38451  dihmeetlem3N  38456  dihmeetlem13N  38470  pellex  39452