Theorem simpl1 1003

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

Assertion

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

Proof of Theorem simpl1

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

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

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 983

This theorem is referenced by:  simpll1  1039  simprl1  1045  simp1l1  1093  simp2l1  1099  simp3l1  1105  3anandirs  1361  rspc3ev  2895  brcogw  4851  cocan1  5863  oawordi  6562  nnmord  6610  nnmword  6611  dif1en  6983  ac6sfi  7002  ordiso2  7144  difinfsn  7209  ctssdc  7222  2omotaplemap  7376  enq0tr  7554  distrlem4prl  7704  distrlem4pru  7705  ltaprg  7739  aptiprlemu  7760  lelttr  8168  readdcan  8219  addcan  8259  addcan2  8260  ltadd2  8499  ltmul1a  8671  ltmul1  8672  divmulassap  8775  divmulasscomap  8776  lemul1a  8938  xrlelttr  9935  xleadd1a  10002  xlesubadd  10012  icoshftf1o  10120  lincmb01cmp  10132  iccf1o  10133  fztri3or  10168  fzofzim  10319  ioom  10410  modqmuladdim  10519  modqm1p1mod0  10527  q2submod  10537  modqaddmulmod  10543  ltexp2a  10743  exple1  10747  expnlbnd2  10817  nn0ltexp2  10861  nn0leexp2  10862  expcan  10868  fiprsshashgt1  10969  fimaxq  10979  fun2dmnop0  10999  ccatass  11072  swrdlen  11113  swrdfv  11114  swrdswrdlem  11163  maxleastb  11569  maxltsup  11573  xrltmaxsup  11612  xrmaxltsup  11613  xrmaxaddlem  11615  addcn2  11665  mulcn2  11667  dvdsmodexp  12150  dvdsadd2b  12195  dvdsmod  12217  oexpneg  12232  divalglemex  12277  divalg  12279  gcdass  12380  rplpwr  12392  rppwr  12393  nnwodc  12401  coprmdvds2  12459  rpmulgcd2  12461  qredeq  12462  rpdvds  12465  cncongr2  12470  rpexp  12519  znege1  12544  prmdiveq  12602  hashgcdlem  12604  odzdvds  12612  modprmn0modprm0  12623  coprimeprodsq2  12625  pythagtriplem3  12634  pcdvdsb  12687  pcgcd1  12695  qexpz  12719  pockthg  12724  ctinf  12845  nninfdc  12868  unbendc  12869  isnsgrp  13282  issubmnd  13318  ress0g  13319  mulgneg  13520  mulgdirlem  13533  submmulg  13546  subgmulg  13568  nmzsubg  13590  ghmmulg  13636  srg1zr  13793  ring1eq0  13854  mulgass2  13864  rhmdvdsr  13981  rmodislmodlem  14156  rmodislmod  14157  lssintclm  14190  rnglidlrng  14304  2idlcpblrng  14329  neiint  14661  topssnei  14678  iscnp4  14734  cnptopco  14738  cnconst2  14749  cnrest2  14752  cnptoprest  14755  cnpdis  14758  bldisj  14917  blgt0  14918  bl2in  14919  blss2ps  14922  blss2  14923  xblm  14933  blssps  14943  blss  14944  xmetresbl  14956  bdbl  15019  metcnp3  15027  metcnp2  15029  cncfmptc  15112  dvcnp2cntop  15215  dvcn  15216  logdivlti  15397  ltexp2  15457  lgsfcl2  15527  lgsdilem  15548  lgsdirprm  15555  lgsdir  15556  lgsdi  15558  lgsne0  15559  incistruhgr  15730