Theorem simpl1 1024

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

Assertion

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

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 1021	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	adantr 276	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

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

This theorem is referenced by:  simpll1  1060  simprl1  1066  simp1l1  1114  simp2l1  1120  simp3l1  1126  3anandirs  1382  rspc3ev  2925  brcogw  4897  cocan1  5923  oawordi  6632  nnmord  6680  nnmword  6681  dif1en  7063  ac6sfi  7082  ordiso2  7228  difinfsn  7293  ctssdc  7306  2omotaplemap  7469  enq0tr  7647  distrlem4prl  7797  distrlem4pru  7798  ltaprg  7832  aptiprlemu  7853  lelttr  8261  readdcan  8312  addcan  8352  addcan2  8353  ltadd2  8592  ltmul1a  8764  ltmul1  8765  divmulassap  8868  divmulasscomap  8869  lemul1a  9031  xrlelttr  10034  xleadd1a  10101  xlesubadd  10111  icoshftf1o  10219  lincmb01cmp  10231  iccf1o  10232  fztri3or  10267  fzofzim  10420  ioom  10513  modqmuladdim  10622  modqm1p1mod0  10630  q2submod  10640  modqaddmulmod  10646  ltexp2a  10846  exple1  10850  expnlbnd2  10920  nn0ltexp2  10964  nn0leexp2  10965  expcan  10971  fiprsshashgt1  11074  fimaxq  11084  fun2dmnop0  11104  ccatass  11178  swrdlen  11226  swrdfv  11227  swrdswrdlem  11278  ccatopth  11290  maxleastb  11768  maxltsup  11772  xrltmaxsup  11811  xrmaxltsup  11812  xrmaxaddlem  11814  addcn2  11864  mulcn2  11866  dvdsmodexp  12349  dvdsadd2b  12394  dvdsmod  12416  oexpneg  12431  divalglemex  12476  divalg  12478  gcdass  12579  rplpwr  12591  rppwr  12592  nnwodc  12600  coprmdvds2  12658  rpmulgcd2  12660  qredeq  12661  rpdvds  12664  cncongr2  12669  rpexp  12718  znege1  12743  prmdiveq  12801  hashgcdlem  12803  odzdvds  12811  modprmn0modprm0  12822  coprimeprodsq2  12824  pythagtriplem3  12833  pcdvdsb  12886  pcgcd1  12894  qexpz  12918  pockthg  12923  ctinf  13044  nninfdc  13067  unbendc  13068  isnsgrp  13482  issubmnd  13518  ress0g  13519  mulgneg  13720  mulgdirlem  13733  submmulg  13746  subgmulg  13768  nmzsubg  13790  ghmmulg  13836  srg1zr  13993  ring1eq0  14054  mulgass2  14064  rhmdvdsr  14182  rmodislmodlem  14357  rmodislmod  14358  lssintclm  14391  rnglidlrng  14505  2idlcpblrng  14530  neiint  14862  topssnei  14879  iscnp4  14935  cnptopco  14939  cnconst2  14950  cnrest2  14953  cnptoprest  14956  cnpdis  14959  bldisj  15118  blgt0  15119  bl2in  15120  blss2ps  15123  blss2  15124  xblm  15134  blssps  15144  blss  15145  xmetresbl  15157  bdbl  15220  metcnp3  15228  metcnp2  15230  cncfmptc  15313  dvcnp2cntop  15416  dvcn  15417  logdivlti  15598  ltexp2  15658  lgsfcl2  15728  lgsdilem  15749  lgsdirprm  15756  lgsdir  15757  lgsdi  15759  lgsne0  15760  incistruhgr  15934  clwwlkext2edg  16231  clwwlknonex2e  16249