Theorem simp2ll 1241

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tfrlem5  8311  omeu  8512  expmordi  14090  hash7g  14409  4sqlem18  16890  vdwlem10  16918  0catg  17611  mvrf1  21941  mdetuni0  22565  mdetmul  22567  tsmsxp  24099  ax5seglem3  29004  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem12  36292  btwnconn1lem13  36293  lshpkrlem6  39371  athgt  39712  2llnjN  39823  dalaw  40142  lhpmcvr4N  40282  cdlemb2  40297  4atexlemex6  40330  cdlemd7  40460  cdleme01N  40477  cdleme02N  40478  cdleme0ex1N  40479  cdleme0ex2N  40480  cdleme7aa  40498  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme11a  40516  cdleme20k  40575  cdleme27cl  40622  cdleme42e  40735  cdleme42h  40738  cdleme42i  40739  cdlemf  40819  cdlemg2kq  40858  cdlemg2m  40860  cdlemg8a  40883  cdlemg11aq  40894  cdlemg10c  40895  cdlemg11b  40898  cdlemg17a  40917  cdlemg31b0N  40950  cdlemg31c  40955  cdlemg33c0  40958  cdlemg41  40974  cdlemh2  41072  cdlemn9  41461  dihglbcpreN  41556  dihmeetlem3N  41561  dihmeetlem13N  41575  pellex  43073