Theorem simpl1 1031

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

Assertion

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

Proof of Theorem simpl1

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll1  1067  simprl1  1073  simp1l1  1121  simp2l1  1127  simp3l1  1133  3anandirs  1389  rspc3ev  2947  brcogw  4951  cocan1  5996  oawordi  6746  nnmord  6794  nnmword  6795  mapunen  7156  dif1en  7188  ac6sfi  7207  ordiso2  7382  difinfsn  7447  ctssdc  7460  2omotaplemap  7630  enq0tr  7808  distrlem4prl  7958  distrlem4pru  7959  ltaprg  7993  aptiprlemu  8014  lelttr  8421  readdcan  8474  addcan  8514  addcan2  8515  ltadd2  8755  ltmul1a  8928  ltmul1  8929  divmulassap  9034  divmulasscomap  9035  lemul1a  9197  xrlelttr  10226  xleadd1a  10293  xlesubadd  10303  icoshftf1o  10411  lincmb01cmp  10423  lincmble  10424  iccf1o  10425  fztri3or  10461  nn0p1elfzo  10612  fzofzim  10618  ioom  10713  modqmuladdim  10826  modqm1p1mod0  10834  q2submod  10844  modqaddmulmod  10850  ltexp2a  11050  exple1  11054  expnlbnd2  11125  nn0ltexp2  11170  nn0leexp2  11171  expcan  11177  fiprsshashgt1  11281  fimaxq  11293  hashtpgim  11320  hashtpg  11322  fun2dmnop0  11325  ccatass  11399  swrdlen  11447  swrdfv  11448  swrdswrdlem  11499  ccatopth  11511  maxleastb  12004  maxltsup  12008  xrltmaxsup  12049  xrmaxltsup  12050  xrmaxaddlem  12052  addcn2  12102  mulcn2  12104  dvdsmodexp  12588  dvdsadd2b  12633  dvdsmod  12655  oexpneg  12670  divalglemex  12715  divalg  12717  gcdass  12818  rplpwr  12830  rppwr  12831  nnwodc  12839  coprmdvds2  12897  rpmulgcd2  12899  qredeq  12900  rpdvds  12903  cncongr2  12908  rpexp  12958  znege1  12984  prmdiveq  13044  hashgcdlem  13046  odzdvds  13054  modprmn0modprm0  13065  coprimeprodsq2  13067  pythagtriplem3  13076  pcdvdsb  13129  pcgcd1  13137  qexpz  13161  pockthg  13166  ctinf  13380  nninfdc  13403  unbendc  13404  isnsgrp  13781  issubmnd  13815  ress0g  13816  mulgneg  14003  mulgdirlem  14016  submmulg  14029  subgmulg  14051  nmzsubg  14073  ghmmulg  14119  ring1eq0  14461  mulgass2  14471  rhmdvdsr  14592  rmodislmodlem  14797  rmodislmod  14798  lssintclm  14831  rnglidlrng  14945  2idlcpblrng  14970  issubassa  15123  snifpsrbagfi  15170  neiint  15383  topssnei  15400  iscnp4  15456  cnptopco  15460  cnconst2  15471  cnrest2  15474  cnptoprest  15477  cnpdis  15480  bldisj  15639  blgt0  15640  bl2in  15641  blss2ps  15644  blss2  15645  xblm  15655  blssps  15665  blss  15666  xmetresbl  15678  bdbl  15741  metcnp3  15749  metcnp2  15751  cncfmptc  15834  dvcnp2cntop  15937  dvcn  15938  logdivlti  16123  ltexp2  16189  pellexlem2  16242  bcmono  16316  lgsfcl2  16342  lgsdilem  16363  lgsdirprm  16370  lgsdir  16371  lgsdi  16373  lgsne0  16374  incistruhgr  16548  clwwlkext2edg  16880  clwwlknonex2e  16898