Theorem simp1l 1048

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 1045	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

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

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 1007

This theorem is referenced by:  simpl1l  1075  simpr1l  1081  simp11l  1135  simp21l  1141  simp31l  1147  en2lp  4681  tfisi  4714  funprg  5411  nnsucsssuc  6738  ecopovtrn  6879  ecopovtrng  6882  addassnqg  7713  distrnqg  7718  ltsonq  7729  ltanqg  7731  ltmnqg  7732  distrnq0  7790  addassnq0  7793  mulasssrg  8089  distrsrg  8090  lttrsr  8093  ltsosr  8095  ltasrg  8101  mulextsr1lem  8111  mulextsr1  8112  axmulass  8204  axdistr  8205  dmdcanap  9016  lt2msq1  9179  ltdiv2  9181  lediv2  9185  xaddass  10224  xaddass2  10225  xlt2add  10235  modqdi  10781  expaddzaplem  10971  expaddzap  10972  expmulzap  10974  swrdspsleq  11387  pfxeq  11416  ccatopth2  11437  pfxccat3  11454  resqrtcl  11743  bdtrilem  11953  bdtri  11954  xrbdtri  11990  bitsfzo  12670  prmexpb  12877  4sqlem18  13135  subgabl  14089  rng1zrlem  14202  opprringbg  14327  cnptoprest  15234  ssblps  15420  ssbl  15421  plyadd  15746  plymul  15747  rplogbchbase  15945  rplogbreexp  15948  relogbcxpbap  15960  lgssq  16043  uhgr2edg  16331  clwwlkccat  16526