Theorem simpl1 1002

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

Assertion

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

Proof of Theorem simpl1

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

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

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 982

This theorem is referenced by:  simpll1  1038  simprl1  1044  simp1l1  1092  simp2l1  1098  simp3l1  1104  3anandirs  1359  rspc3ev  2885  brcogw  4836  cocan1  5835  oawordi  6528  nnmord  6576  nnmword  6577  dif1en  6941  ac6sfi  6960  ordiso2  7102  difinfsn  7167  ctssdc  7180  2omotaplemap  7326  enq0tr  7503  distrlem4prl  7653  distrlem4pru  7654  ltaprg  7688  aptiprlemu  7709  lelttr  8117  readdcan  8168  addcan  8208  addcan2  8209  ltadd2  8448  ltmul1a  8620  ltmul1  8621  divmulassap  8724  divmulasscomap  8725  lemul1a  8887  xrlelttr  9883  xleadd1a  9950  xlesubadd  9960  icoshftf1o  10068  lincmb01cmp  10080  iccf1o  10081  fztri3or  10116  fzofzim  10266  ioom  10352  modqmuladdim  10461  modqm1p1mod0  10469  q2submod  10479  modqaddmulmod  10485  ltexp2a  10685  exple1  10689  expnlbnd2  10759  nn0ltexp2  10803  nn0leexp2  10804  expcan  10810  fiprsshashgt1  10911  fimaxq  10921  maxleastb  11381  maxltsup  11385  xrltmaxsup  11424  xrmaxltsup  11425  xrmaxaddlem  11427  addcn2  11477  mulcn2  11479  dvdsmodexp  11962  dvdsadd2b  12007  dvdsmod  12029  oexpneg  12044  divalglemex  12089  divalg  12091  gcdass  12192  rplpwr  12204  rppwr  12205  nnwodc  12213  coprmdvds2  12271  rpmulgcd2  12273  qredeq  12274  rpdvds  12277  cncongr2  12282  rpexp  12331  znege1  12356  prmdiveq  12414  hashgcdlem  12416  odzdvds  12424  modprmn0modprm0  12435  coprimeprodsq2  12437  pythagtriplem3  12446  pcdvdsb  12499  pcgcd1  12507  qexpz  12531  pockthg  12536  ctinf  12657  nninfdc  12680  unbendc  12681  isnsgrp  13059  issubmnd  13093  ress0g  13094  mulgneg  13280  mulgdirlem  13293  submmulg  13306  subgmulg  13328  nmzsubg  13350  ghmmulg  13396  srg1zr  13553  ring1eq0  13614  mulgass2  13624  rhmdvdsr  13741  rmodislmodlem  13916  rmodislmod  13917  lssintclm  13950  rnglidlrng  14064  2idlcpblrng  14089  neiint  14391  topssnei  14408  iscnp4  14464  cnptopco  14468  cnconst2  14479  cnrest2  14482  cnptoprest  14485  cnpdis  14488  bldisj  14647  blgt0  14648  bl2in  14649  blss2ps  14652  blss2  14653  xblm  14663  blssps  14673  blss  14674  xmetresbl  14686  bdbl  14749  metcnp3  14757  metcnp2  14759  cncfmptc  14842  dvcnp2cntop  14945  dvcn  14946  logdivlti  15127  ltexp2  15187  lgsfcl2  15257  lgsdilem  15278  lgsdirprm  15285  lgsdir  15286  lgsdi  15288  lgsne0  15289