Theorem simp1l 1047

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1l	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1044	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  simpl1l  1074  simpr1l  1080  simp11l  1134  simp21l  1140  simp31l  1146  en2lp  4652  tfisi  4685  funprg  5380  nnsucsssuc  6660  ecopovtrn  6801  ecopovtrng  6804  addassnqg  7602  distrnqg  7607  ltsonq  7618  ltanqg  7620  ltmnqg  7621  distrnq0  7679  addassnq0  7682  mulasssrg  7978  distrsrg  7979  lttrsr  7982  ltsosr  7984  ltasrg  7990  mulextsr1lem  8000  mulextsr1  8001  axmulass  8093  axdistr  8094  dmdcanap  8902  lt2msq1  9065  ltdiv2  9067  lediv2  9071  xaddass  10104  xaddass2  10105  xlt2add  10115  modqdi  10655  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  swrdspsleq  11252  pfxeq  11281  ccatopth2  11302  pfxccat3  11319  resqrtcl  11594  bdtrilem  11804  bdtri  11805  xrbdtri  11841  bitsfzo  12521  prmexpb  12728  4sqlem18  12986  subgabl  13924  opprringbg  14099  cnptoprest  14969  ssblps  15155  ssbl  15156  plyadd  15481  plymul  15482  rplogbchbase  15680  rplogbreexp  15683  relogbcxpbap  15695  lgssq  15775  uhgr2edg  16063  clwwlkccat  16258