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  4949  cocan1  5993  oawordi  6742  nnmord  6790  nnmword  6791  mapunen  7151  dif1en  7183  ac6sfi  7202  ordiso2  7375  difinfsn  7440  ctssdc  7453  2omotaplemap  7623  enq0tr  7801  distrlem4prl  7951  distrlem4pru  7952  ltaprg  7986  aptiprlemu  8007  lelttr  8414  readdcan  8466  addcan  8506  addcan2  8507  ltadd2  8747  ltmul1a  8920  ltmul1  8921  divmulassap  9026  divmulasscomap  9027  lemul1a  9189  xrlelttr  10210  xleadd1a  10277  xlesubadd  10287  icoshftf1o  10395  lincmb01cmp  10407  lincmble  10408  iccf1o  10409  fztri3or  10445  nn0p1elfzo  10596  fzofzim  10602  ioom  10697  modqmuladdim  10806  modqm1p1mod0  10814  q2submod  10824  modqaddmulmod  10830  ltexp2a  11030  exple1  11034  expnlbnd2  11105  nn0ltexp2  11149  nn0leexp2  11150  expcan  11156  fiprsshashgt1  11260  fimaxq  11272  hashtpgim  11299  hashtpg  11301  fun2dmnop0  11304  ccatass  11378  swrdlen  11426  swrdfv  11427  swrdswrdlem  11478  ccatopth  11490  maxleastb  11982  maxltsup  11986  xrltmaxsup  12025  xrmaxltsup  12026  xrmaxaddlem  12028  addcn2  12078  mulcn2  12080  dvdsmodexp  12564  dvdsadd2b  12609  dvdsmod  12631  oexpneg  12646  divalglemex  12691  divalg  12693  gcdass  12794  rplpwr  12806  rppwr  12807  nnwodc  12815  coprmdvds2  12873  rpmulgcd2  12875  qredeq  12876  rpdvds  12879  cncongr2  12884  rpexp  12933  znege1  12958  prmdiveq  13016  hashgcdlem  13018  odzdvds  13026  modprmn0modprm0  13037  coprimeprodsq2  13039  pythagtriplem3  13048  pcdvdsb  13101  pcgcd1  13109  qexpz  13133  pockthg  13138  ctinf  13323  nninfdc  13346  unbendc  13347  isnsgrp  13723  issubmnd  13757  ress0g  13758  mulgneg  13945  mulgdirlem  13958  submmulg  13971  subgmulg  13993  nmzsubg  14015  ghmmulg  14061  ring1eq0  14355  mulgass2  14365  rhmdvdsr  14484  rmodislmodlem  14689  rmodislmod  14690  lssintclm  14723  rnglidlrng  14837  2idlcpblrng  14862  issubassa  15015  neiint  15248  topssnei  15265  iscnp4  15321  cnptopco  15325  cnconst2  15336  cnrest2  15339  cnptoprest  15342  cnpdis  15345  bldisj  15504  blgt0  15505  bl2in  15506  blss2ps  15509  blss2  15510  xblm  15520  blssps  15530  blss  15531  xmetresbl  15543  bdbl  15606  metcnp3  15614  metcnp2  15616  cncfmptc  15699  dvcnp2cntop  15802  dvcn  15803  logdivlti  15986  ltexp2  16049  pellexlem2  16098  bcmono  16124  lgsfcl2  16137  lgsdilem  16158  lgsdirprm  16165  lgsdir  16166  lgsdi  16168  lgsne0  16169  incistruhgr  16343  clwwlkext2edg  16675  clwwlknonex2e  16693