Theorem simp2ll 1238

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

Assertion

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

Proof of Theorem simp2ll

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  tfrlem5  8231  omeu  8436  expmordi  13913  4sqlem18  16691  vdwlem10  16719  0catg  17425  mvrf1  21222  mdetuni0  21798  mdetmul  21800  tsmsxp  23334  ax5seglem3  27327  btwnconn1lem1  34417  btwnconn1lem2  34418  btwnconn1lem3  34419  btwnconn1lem12  34428  btwnconn1lem13  34429  lshpkrlem6  37155  athgt  37496  2llnjN  37607  dalaw  37926  lhpmcvr4N  38066  cdlemb2  38081  4atexlemex6  38114  cdlemd7  38244  cdleme01N  38261  cdleme02N  38262  cdleme0ex1N  38263  cdleme0ex2N  38264  cdleme7aa  38282  cdleme7c  38285  cdleme7d  38286  cdleme7e  38287  cdleme7ga  38288  cdleme7  38289  cdleme11a  38300  cdleme20k  38359  cdleme27cl  38406  cdleme42e  38519  cdleme42h  38522  cdleme42i  38523  cdlemf  38603  cdlemg2kq  38642  cdlemg2m  38644  cdlemg8a  38667  cdlemg11aq  38678  cdlemg10c  38679  cdlemg11b  38682  cdlemg17a  38701  cdlemg31b0N  38734  cdlemg31c  38739  cdlemg33c0  38742  cdlemg41  38758  cdlemh2  38856  cdlemn9  39245  dihglbcpreN  39340  dihmeetlem3N  39345  dihmeetlem13N  39359  pellex  40680