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 778	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant2 1152	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  tfrlem5  8367  omeu  8571  expmordi  14205  hash7g  14525  4sqlem18  17023  vdwlem10  17051  0catg  17745  mvrf1  22116  mdetuni0  22759  mdetmul  22761  tsmsxp  24293  ax5seglem3  29262  btwnconn1lem1  36560  btwnconn1lem2  36561  btwnconn1lem3  36562  btwnconn1lem12  36571  btwnconn1lem13  36572  lshpkrlem6  39870  athgt  40211  2llnjN  40322  dalaw  40641  lhpmcvr4N  40781  cdlemb2  40796  4atexlemex6  40829  cdlemd7  40959  cdleme01N  40976  cdleme02N  40977  cdleme0ex1N  40978  cdleme0ex2N  40979  cdleme7aa  40997  cdleme7c  41000  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme11a  41015  cdleme20k  41074  cdleme27cl  41121  cdleme42e  41234  cdleme42h  41237  cdleme42i  41238  cdlemf  41318  cdlemg2kq  41357  cdlemg2m  41359  cdlemg8a  41382  cdlemg11aq  41393  cdlemg10c  41394  cdlemg11b  41397  cdlemg17a  41416  cdlemg31b0N  41449  cdlemg31c  41454  cdlemg33c0  41457  cdlemg41  41473  cdlemh2  41571  cdlemn9  41960  dihglbcpreN  42055  dihmeetlem3N  42060  dihmeetlem13N  42074  pellex  43545