Theorem simpl1 1000

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 997	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	adantr 276	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simpll1  1036  simprl1  1042  simp1l1  1090  simp2l1  1096  simp3l1  1102  3anandirs  1348  rspc3ev  2860  brcogw  4798  cocan1  5790  oawordi  6472  nnmord  6520  nnmword  6521  dif1en  6881  ac6sfi  6900  ordiso2  7036  difinfsn  7101  ctssdc  7114  2omotaplemap  7258  enq0tr  7435  distrlem4prl  7585  distrlem4pru  7586  ltaprg  7620  aptiprlemu  7641  lelttr  8048  readdcan  8099  addcan  8139  addcan2  8140  ltadd2  8378  ltmul1a  8550  ltmul1  8551  divmulassap  8654  divmulasscomap  8655  lemul1a  8817  xrlelttr  9808  xleadd1a  9875  xlesubadd  9885  icoshftf1o  9993  lincmb01cmp  10005  iccf1o  10006  fztri3or  10041  fzofzim  10190  ioom  10263  modqmuladdim  10369  modqm1p1mod0  10377  q2submod  10387  modqaddmulmod  10393  ltexp2a  10574  exple1  10578  expnlbnd2  10648  nn0ltexp2  10691  nn0leexp2  10692  expcan  10698  fiprsshashgt1  10799  fimaxq  10809  maxleastb  11225  maxltsup  11229  xrltmaxsup  11267  xrmaxltsup  11268  xrmaxaddlem  11270  addcn2  11320  mulcn2  11322  dvdsmodexp  11804  dvdsadd2b  11849  dvdsmod  11870  oexpneg  11884  divalglemex  11929  divalg  11931  gcdass  12018  rplpwr  12030  rppwr  12031  nnwodc  12039  coprmdvds2  12095  rpmulgcd2  12097  qredeq  12098  rpdvds  12101  cncongr2  12106  rpexp  12155  znege1  12180  prmdiveq  12238  hashgcdlem  12240  odzdvds  12247  modprmn0modprm0  12258  coprimeprodsq2  12260  pythagtriplem3  12269  pcdvdsb  12321  pcgcd1  12329  qexpz  12352  pockthg  12357  ctinf  12433  nninfdc  12456  unbendc  12457  isnsgrp  12817  issubmnd  12848  ress0g  12849  mulgneg  13006  mulgdirlem  13019  subgmulg  13053  nmzsubg  13075  srg1zr  13175  ring1eq0  13230  mulgass2  13240  rmodislmodlem  13445  rmodislmod  13446  lssintclm  13476  neiint  13730  topssnei  13747  iscnp4  13803  cnptopco  13807  cnconst2  13818  cnrest2  13821  cnptoprest  13824  cnpdis  13827  bldisj  13986  blgt0  13987  bl2in  13988  blss2ps  13991  blss2  13992  xblm  14002  blssps  14012  blss  14013  xmetresbl  14025  bdbl  14088  metcnp3  14096  metcnp2  14098  cncfmptc  14167  dvcnp2cntop  14248  dvcn  14249  logdivlti  14387  ltexp2  14445  lgsfcl2  14492  lgsdilem  14513  lgsdirprm  14520  lgsdir  14521  lgsdi  14523  lgsne0  14524