Theorem simp1l 1052

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl1l  1079  simpr1l  1085  simp11l  1139  simp21l  1145  simp31l  1151  en2lp  4703  tfisi  4736  funprg  5434  nnsucsssuc  6769  ecopovtrn  6910  ecopovtrng  6913  addassnqg  7756  distrnqg  7761  ltsonq  7772  ltanqg  7774  ltmnqg  7775  distrnq0  7833  addassnq0  7836  mulasssrg  8132  distrsrg  8133  lttrsr  8136  ltsosr  8138  ltasrg  8144  mulextsr1lem  8154  mulextsr1  8155  axmulass  8247  axdistr  8248  dmdcanap  9061  lt2msq1  9224  ltdiv2  9226  lediv2  9230  xaddass  10289  xaddass2  10290  xlt2add  10300  modqdi  10851  expaddzaplem  11041  expaddzap  11042  expmulzap  11044  swrdspsleq  11462  pfxeq  11491  ccatopth2  11512  pfxccat3  11529  resqrtcl  11818  bdtrilem  12031  bdtri  12032  xrbdtri  12068  bitsfzo  12748  prmexpb  12956  4sqlem18  13217  subgabl  14227  rng1zrlem  14366  opprringbg  14495  cnptoprest  15477  ssblps  15663  ssbl  15664  plyadd  15989  plymul  15990  rplogbchbase  16198  rplogbreexp  16201  relogbcxpbap  16213  lgssq  16376  uhgr2edg  16664  clwwlkccat  16859