Theorem simpl1 1027

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

Assertion

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

Proof of Theorem simpl1

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

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

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 1007

This theorem is referenced by:  simpll1  1063  simprl1  1069  simp1l1  1117  simp2l1  1123  simp3l1  1129  3anandirs  1385  rspc3ev  2937  brcogw  4923  cocan1  5959  oawordi  6701  nnmord  6749  nnmword  6750  mapunen  7103  dif1en  7135  ac6sfi  7154  ordiso2  7325  difinfsn  7390  ctssdc  7403  2omotaplemap  7567  enq0tr  7745  distrlem4prl  7895  distrlem4pru  7896  ltaprg  7930  aptiprlemu  7951  lelttr  8358  readdcan  8409  addcan  8449  addcan2  8450  ltadd2  8689  ltmul1a  8861  ltmul1  8862  divmulassap  8965  divmulasscomap  8966  lemul1a  9128  xrlelttr  10135  xleadd1a  10202  xlesubadd  10212  icoshftf1o  10320  lincmb01cmp  10332  lincmble  10333  iccf1o  10334  fztri3or  10369  nn0p1elfzo  10517  fzofzim  10523  ioom  10616  modqmuladdim  10725  modqm1p1mod0  10733  q2submod  10743  modqaddmulmod  10749  ltexp2a  10949  exple1  10953  expnlbnd2  11023  nn0ltexp2  11067  nn0leexp2  11068  expcan  11074  fiprsshashgt1  11177  fimaxq  11187  hashtpgim  11210  hashtpg  11212  fun2dmnop0  11215  ccatass  11289  swrdlen  11337  swrdfv  11338  swrdswrdlem  11389  ccatopth  11401  maxleastb  11892  maxltsup  11896  xrltmaxsup  11935  xrmaxltsup  11936  xrmaxaddlem  11938  addcn2  11988  mulcn2  11990  dvdsmodexp  12474  dvdsadd2b  12519  dvdsmod  12541  oexpneg  12556  divalglemex  12601  divalg  12603  gcdass  12704  rplpwr  12716  rppwr  12717  nnwodc  12725  coprmdvds2  12783  rpmulgcd2  12785  qredeq  12786  rpdvds  12789  cncongr2  12794  rpexp  12843  znege1  12868  prmdiveq  12926  hashgcdlem  12928  odzdvds  12936  modprmn0modprm0  12947  coprimeprodsq2  12949  pythagtriplem3  12958  pcdvdsb  13011  pcgcd1  13019  qexpz  13043  pockthg  13048  ctinf  13170  nninfdc  13193  unbendc  13194  isnsgrp  13608  issubmnd  13644  ress0g  13645  mulgneg  13846  mulgdirlem  13859  submmulg  13872  subgmulg  13894  nmzsubg  13916  ghmmulg  13962  srg1zr  14120  ring1eq0  14181  mulgass2  14191  rhmdvdsr  14309  rmodislmodlem  14485  rmodislmod  14486  lssintclm  14519  rnglidlrng  14633  2idlcpblrng  14658  neiint  14997  topssnei  15014  iscnp4  15070  cnptopco  15074  cnconst2  15085  cnrest2  15088  cnptoprest  15091  cnpdis  15094  bldisj  15253  blgt0  15254  bl2in  15255  blss2ps  15258  blss2  15259  xblm  15269  blssps  15279  blss  15280  xmetresbl  15292  bdbl  15355  metcnp3  15363  metcnp2  15365  cncfmptc  15448  dvcnp2cntop  15551  dvcn  15552  logdivlti  15733  ltexp2  15793  pellexlem2  15833  lgsfcl2  15866  lgsdilem  15887  lgsdirprm  15894  lgsdir  15895  lgsdi  15897  lgsne0  15898  incistruhgr  16072  clwwlkext2edg  16404  clwwlknonex2e  16422