Theorem simp3ll 1241

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

Assertion

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

Proof of Theorem simp3ll

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  f1oiso2  7084  omeu  8194  ntrivcvgmul  15250  tsmsxp  22760  tgqioo  23405  ovolunlem2  24102  plyadd  24814  plymul  24815  coeeu  24822  tghilberti2  26432  nosupbnd1lem2  33322  btwnconn1lem2  33662  btwnconn1lem3  33663  btwnconn1lem12  33672  athgt  36752  2llnjN  36863  4atlem12b  36907  lncmp  37079  cdlema2N  37088  cdlemc2  37488  cdleme5  37536  cdleme11a  37556  cdleme21ct  37625  cdleme21  37633  cdleme22eALTN  37641  cdleme24  37648  cdleme27cl  37662  cdleme27a  37663  cdleme28  37669  cdleme36a  37756  cdleme42b  37774  cdleme48fvg  37796  cdlemf  37859  cdlemk39  38212  cdlemkid1  38218  dihlsscpre  38530  dihord4  38554  dihord5apre  38558  dihmeetlem20N  38622  mapdh9a  39085  pellex  39776  jm2.27  39949