Theorem simpl1 1002

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

Assertion

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

Proof of Theorem simpl1

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

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

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 982

This theorem is referenced by:  simpll1  1038  simprl1  1044  simp1l1  1092  simp2l1  1098  simp3l1  1104  3anandirs  1359  rspc3ev  2885  brcogw  4836  cocan1  5837  oawordi  6536  nnmord  6584  nnmword  6585  dif1en  6949  ac6sfi  6968  ordiso2  7110  difinfsn  7175  ctssdc  7188  2omotaplemap  7342  enq0tr  7520  distrlem4prl  7670  distrlem4pru  7671  ltaprg  7705  aptiprlemu  7726  lelttr  8134  readdcan  8185  addcan  8225  addcan2  8226  ltadd2  8465  ltmul1a  8637  ltmul1  8638  divmulassap  8741  divmulasscomap  8742  lemul1a  8904  xrlelttr  9900  xleadd1a  9967  xlesubadd  9977  icoshftf1o  10085  lincmb01cmp  10097  iccf1o  10098  fztri3or  10133  fzofzim  10283  ioom  10369  modqmuladdim  10478  modqm1p1mod0  10486  q2submod  10496  modqaddmulmod  10502  ltexp2a  10702  exple1  10706  expnlbnd2  10776  nn0ltexp2  10820  nn0leexp2  10821  expcan  10827  fiprsshashgt1  10928  fimaxq  10938  maxleastb  11398  maxltsup  11402  xrltmaxsup  11441  xrmaxltsup  11442  xrmaxaddlem  11444  addcn2  11494  mulcn2  11496  dvdsmodexp  11979  dvdsadd2b  12024  dvdsmod  12046  oexpneg  12061  divalglemex  12106  divalg  12108  gcdass  12209  rplpwr  12221  rppwr  12222  nnwodc  12230  coprmdvds2  12288  rpmulgcd2  12290  qredeq  12291  rpdvds  12294  cncongr2  12299  rpexp  12348  znege1  12373  prmdiveq  12431  hashgcdlem  12433  odzdvds  12441  modprmn0modprm0  12452  coprimeprodsq2  12454  pythagtriplem3  12463  pcdvdsb  12516  pcgcd1  12524  qexpz  12548  pockthg  12553  ctinf  12674  nninfdc  12697  unbendc  12698  isnsgrp  13110  issubmnd  13146  ress0g  13147  mulgneg  13348  mulgdirlem  13361  submmulg  13374  subgmulg  13396  nmzsubg  13418  ghmmulg  13464  srg1zr  13621  ring1eq0  13682  mulgass2  13692  rhmdvdsr  13809  rmodislmodlem  13984  rmodislmod  13985  lssintclm  14018  rnglidlrng  14132  2idlcpblrng  14157  neiint  14489  topssnei  14506  iscnp4  14562  cnptopco  14566  cnconst2  14577  cnrest2  14580  cnptoprest  14583  cnpdis  14586  bldisj  14745  blgt0  14746  bl2in  14747  blss2ps  14750  blss2  14751  xblm  14761  blssps  14771  blss  14772  xmetresbl  14784  bdbl  14847  metcnp3  14855  metcnp2  14857  cncfmptc  14940  dvcnp2cntop  15043  dvcn  15044  logdivlti  15225  ltexp2  15285  lgsfcl2  15355  lgsdilem  15376  lgsdirprm  15383  lgsdir  15384  lgsdi  15386  lgsne0  15387