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  4701  tfisi  4734  funprg  5431  nnsucsssuc  6765  ecopovtrn  6906  ecopovtrng  6909  addassnqg  7749  distrnqg  7754  ltsonq  7765  ltanqg  7767  ltmnqg  7768  distrnq0  7826  addassnq0  7829  mulasssrg  8125  distrsrg  8126  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1lem  8147  mulextsr1  8148  axmulass  8240  axdistr  8241  dmdcanap  9053  lt2msq1  9216  ltdiv2  9218  lediv2  9222  xaddass  10273  xaddass2  10274  xlt2add  10284  modqdi  10831  expaddzaplem  11021  expaddzap  11022  expmulzap  11024  swrdspsleq  11441  pfxeq  11470  ccatopth2  11491  pfxccat3  11508  resqrtcl  11797  bdtrilem  12007  bdtri  12008  xrbdtri  12044  bitsfzo  12724  prmexpb  12931  4sqlem18  13189  subgabl  14138  rng1zrlem  14260  opprringbg  14387  cnptoprest  15342  ssblps  15528  ssbl  15529  plyadd  15854  plymul  15855  rplogbchbase  16058  rplogbreexp  16061  relogbcxpbap  16073  lgssq  16171  uhgr2edg  16459  clwwlkccat  16654