Theorem simp1l 1045

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

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

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 1004

This theorem is referenced by:  simpl1l  1072  simpr1l  1078  simp11l  1132  simp21l  1138  simp31l  1144  en2lp  4647  tfisi  4680  funprg  5374  nnsucsssuc  6651  ecopovtrn  6792  ecopovtrng  6795  addassnqg  7585  distrnqg  7590  ltsonq  7601  ltanqg  7603  ltmnqg  7604  distrnq0  7662  addassnq0  7665  mulasssrg  7961  distrsrg  7962  lttrsr  7965  ltsosr  7967  ltasrg  7973  mulextsr1lem  7983  mulextsr1  7984  axmulass  8076  axdistr  8077  dmdcanap  8885  lt2msq1  9048  ltdiv2  9050  lediv2  9054  xaddass  10082  xaddass2  10083  xlt2add  10093  modqdi  10631  expaddzaplem  10821  expaddzap  10822  expmulzap  10824  swrdspsleq  11220  pfxeq  11249  ccatopth2  11270  pfxccat3  11287  resqrtcl  11561  bdtrilem  11771  bdtri  11772  xrbdtri  11808  bitsfzo  12487  prmexpb  12694  4sqlem18  12952  subgabl  13890  opprringbg  14064  cnptoprest  14934  ssblps  15120  ssbl  15121  plyadd  15446  plymul  15447  rplogbchbase  15645  rplogbreexp  15648  relogbcxpbap  15660  lgssq  15740  uhgr2edg  16025  clwwlkccat  16170