Theorem simpl1 1000

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

Assertion

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

Proof of Theorem simpl1

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

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

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 980

This theorem is referenced by:  simpll1  1036  simprl1  1042  simp1l1  1090  simp2l1  1096  simp3l1  1102  3anandirs  1348  rspc3ev  2858  brcogw  4796  cocan1  5787  oawordi  6469  nnmord  6517  nnmword  6518  dif1en  6878  ac6sfi  6897  ordiso2  7033  difinfsn  7098  ctssdc  7111  2omotaplemap  7255  enq0tr  7432  distrlem4prl  7582  distrlem4pru  7583  ltaprg  7617  aptiprlemu  7638  lelttr  8045  readdcan  8096  addcan  8136  addcan2  8137  ltadd2  8375  ltmul1a  8547  ltmul1  8548  divmulassap  8651  divmulasscomap  8652  lemul1a  8814  xrlelttr  9805  xleadd1a  9872  xlesubadd  9882  icoshftf1o  9990  lincmb01cmp  10002  iccf1o  10003  fztri3or  10038  fzofzim  10187  ioom  10260  modqmuladdim  10366  modqm1p1mod0  10374  q2submod  10384  modqaddmulmod  10390  ltexp2a  10571  exple1  10575  expnlbnd2  10645  nn0ltexp2  10688  nn0leexp2  10689  expcan  10695  fiprsshashgt1  10796  fimaxq  10806  maxleastb  11222  maxltsup  11226  xrltmaxsup  11264  xrmaxltsup  11265  xrmaxaddlem  11267  addcn2  11317  mulcn2  11319  dvdsmodexp  11801  dvdsadd2b  11846  dvdsmod  11867  oexpneg  11881  divalglemex  11926  divalg  11928  gcdass  12015  rplpwr  12027  rppwr  12028  nnwodc  12036  coprmdvds2  12092  rpmulgcd2  12094  qredeq  12095  rpdvds  12098  cncongr2  12103  rpexp  12152  znege1  12177  prmdiveq  12235  hashgcdlem  12237  odzdvds  12244  modprmn0modprm0  12255  coprimeprodsq2  12257  pythagtriplem3  12266  pcdvdsb  12318  pcgcd1  12326  qexpz  12349  pockthg  12354  ctinf  12430  nninfdc  12453  unbendc  12454  isnsgrp  12811  issubmnd  12842  ress0g  12843  mulgneg  13000  mulgdirlem  13012  subgmulg  13046  nmzsubg  13068  srg1zr  13168  ring1eq0  13223  mulgass2  13233  neiint  13615  topssnei  13632  iscnp4  13688  cnptopco  13692  cnconst2  13703  cnrest2  13706  cnptoprest  13709  cnpdis  13712  bldisj  13871  blgt0  13872  bl2in  13873  blss2ps  13876  blss2  13877  xblm  13887  blssps  13897  blss  13898  xmetresbl  13910  bdbl  13973  metcnp3  13981  metcnp2  13983  cncfmptc  14052  dvcnp2cntop  14133  dvcn  14134  logdivlti  14272  ltexp2  14330  lgsfcl2  14377  lgsdilem  14398  lgsdirprm  14405  lgsdir  14406  lgsdi  14408  lgsne0  14409