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  4658  tfisi  4691  funprg  5387  nnsucsssuc  6703  ecopovtrn  6844  ecopovtrng  6847  addassnqg  7645  distrnqg  7650  ltsonq  7661  ltanqg  7663  ltmnqg  7664  distrnq0  7722  addassnq0  7725  mulasssrg  8021  distrsrg  8022  lttrsr  8025  ltsosr  8027  ltasrg  8033  mulextsr1lem  8043  mulextsr1  8044  axmulass  8136  axdistr  8137  dmdcanap  8945  lt2msq1  9108  ltdiv2  9110  lediv2  9114  xaddass  10147  xaddass2  10148  xlt2add  10158  modqdi  10698  expaddzaplem  10888  expaddzap  10889  expmulzap  10891  swrdspsleq  11295  pfxeq  11324  ccatopth2  11345  pfxccat3  11362  resqrtcl  11650  bdtrilem  11860  bdtri  11861  xrbdtri  11897  bitsfzo  12577  prmexpb  12784  4sqlem18  13042  subgabl  13980  opprringbg  14155  cnptoprest  15030  ssblps  15216  ssbl  15217  plyadd  15542  plymul  15543  rplogbchbase  15741  rplogbreexp  15744  relogbcxpbap  15756  lgssq  15839  uhgr2edg  16127  clwwlkccat  16322