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

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

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 1011

This theorem is referenced by:  simpl1l  1079  simpr1l  1085  simp11l  1139  simp21l  1145  simp31l  1151  en2lp  4699  tfisi  4732  funprg  5429  nnsucsssuc  6759  ecopovtrn  6900  ecopovtrng  6903  addassnqg  7743  distrnqg  7748  ltsonq  7759  ltanqg  7761  ltmnqg  7762  distrnq0  7820  addassnq0  7823  mulasssrg  8119  distrsrg  8120  lttrsr  8123  ltsosr  8125  ltasrg  8131  mulextsr1lem  8141  mulextsr1  8142  axmulass  8234  axdistr  8235  dmdcanap  9046  lt2msq1  9209  ltdiv2  9211  lediv2  9215  xaddass  10254  xaddass2  10255  xlt2add  10265  modqdi  10812  expaddzaplem  11002  expaddzap  11003  expmulzap  11005  swrdspsleq  11422  pfxeq  11451  ccatopth2  11472  pfxccat3  11489  resqrtcl  11778  bdtrilem  11988  bdtri  11989  xrbdtri  12025  bitsfzo  12705  prmexpb  12912  4sqlem18  13170  subgabl  14119  rng1zrlem  14241  opprringbg  14368  cnptoprest  15323  ssblps  15509  ssbl  15510  plyadd  15835  plymul  15836  rplogbchbase  16035  rplogbreexp  16038  relogbcxpbap  16050  lgssq  16142  uhgr2edg  16430  clwwlkccat  16625