Theorem simp3ll 1132

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

Assertion

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

Proof of Theorem simp3ll

Step	Hyp	Ref	Expression
1		simpll 790	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant3 1084	1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  f1oiso2  6602  omeu  7665  ntrivcvgmul  14634  tsmsxp  21958  tgqioo  22603  ovolunlem2  23266  plyadd  23973  plymul  23974  coeeu  23981  tghilberti2  25533  nosupbnd1lem2  31855  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem12  32205  athgt  34742  2llnjN  34853  4atlem12b  34897  lncmp  35069  cdlema2N  35078  cdlemc2  35479  cdleme5  35527  cdleme11a  35547  cdleme21ct  35617  cdleme21  35625  cdleme22eALTN  35633  cdleme24  35640  cdleme27cl  35654  cdleme27a  35655  cdleme28  35661  cdleme36a  35748  cdleme42b  35766  cdleme48fvg  35788  cdlemf  35851  cdlemk39  36204  cdlemkid1  36210  dihlsscpre  36523  dihord4  36547  dihord5apre  36551  dihmeetlem20N  36615  mapdh9a  37079  pellex  37399  jm2.27  37575