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  4646  tfisi  4679  funprg  5371  nnsucsssuc  6638  ecopovtrn  6779  ecopovtrng  6782  addassnqg  7569  distrnqg  7574  ltsonq  7585  ltanqg  7587  ltmnqg  7588  distrnq0  7646  addassnq0  7649  mulasssrg  7945  distrsrg  7946  lttrsr  7949  ltsosr  7951  ltasrg  7957  mulextsr1lem  7967  mulextsr1  7968  axmulass  8060  axdistr  8061  dmdcanap  8869  lt2msq1  9032  ltdiv2  9034  lediv2  9038  xaddass  10065  xaddass2  10066  xlt2add  10076  modqdi  10614  expaddzaplem  10804  expaddzap  10805  expmulzap  10807  swrdspsleq  11199  pfxeq  11228  ccatopth2  11249  pfxccat3  11266  resqrtcl  11540  bdtrilem  11750  bdtri  11751  xrbdtri  11787  bitsfzo  12466  prmexpb  12673  4sqlem18  12931  subgabl  13869  opprringbg  14043  cnptoprest  14913  ssblps  15099  ssbl  15100  plyadd  15425  plymul  15426  rplogbchbase  15624  rplogbreexp  15627  relogbcxpbap  15639  lgssq  15719  uhgr2edg  16004