Theorem simp2ll 1259

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

Assertion

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

Proof of Theorem simp2ll

Step	Hyp	Ref	Expression
1		simpll 779	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant2 1152	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfrlem5  8375  omeu  8579  expmordi  14223  hash7g  14543  4sqlem18  17047  vdwlem10  17075  0catg  17769  mvrf1  22172  mdetuni0  22815  mdetmul  22817  tsmsxp  24349  ax5seglem3  29318  btwnconn1lem1  36600  btwnconn1lem2  36601  btwnconn1lem3  36602  btwnconn1lem12  36611  btwnconn1lem13  36612  lshpkrlem6  39930  athgt  40271  2llnjN  40382  dalaw  40701  lhpmcvr4N  40841  cdlemb2  40856  4atexlemex6  40889  cdlemd7  41019  cdleme01N  41036  cdleme02N  41037  cdleme0ex1N  41038  cdleme0ex2N  41039  cdleme7aa  41057  cdleme7c  41060  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme11a  41075  cdleme20k  41134  cdleme27cl  41181  cdleme42e  41294  cdleme42h  41297  cdleme42i  41298  cdlemf  41378  cdlemg2kq  41417  cdlemg2m  41419  cdlemg8a  41442  cdlemg11aq  41453  cdlemg10c  41454  cdlemg11b  41457  cdlemg17a  41476  cdlemg31b0N  41509  cdlemg31c  41514  cdlemg33c0  41517  cdlemg41  41533  cdlemh2  41631  cdlemn9  42020  dihglbcpreN  42115  dihmeetlem3N  42120  dihmeetlem13N  42134  pellex  43603