Theorem simpl1 1027

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

Assertion

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

Proof of Theorem simpl1

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

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

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 1007

This theorem is referenced by:  simpll1  1063  simprl1  1069  simp1l1  1117  simp2l1  1123  simp3l1  1129  3anandirs  1385  rspc3ev  2940  brcogw  4926  cocan1  5962  oawordi  6704  nnmord  6752  nnmword  6753  mapunen  7106  dif1en  7138  ac6sfi  7157  ordiso2  7328  difinfsn  7393  ctssdc  7406  2omotaplemap  7573  enq0tr  7751  distrlem4prl  7901  distrlem4pru  7902  ltaprg  7936  aptiprlemu  7957  lelttr  8364  readdcan  8415  addcan  8455  addcan2  8456  ltadd2  8695  ltmul1a  8867  ltmul1  8868  divmulassap  8971  divmulasscomap  8972  lemul1a  9134  xrlelttr  10142  xleadd1a  10209  xlesubadd  10219  icoshftf1o  10327  lincmb01cmp  10339  lincmble  10340  iccf1o  10341  fztri3or  10376  nn0p1elfzo  10525  fzofzim  10531  ioom  10624  modqmuladdim  10733  modqm1p1mod0  10741  q2submod  10751  modqaddmulmod  10757  ltexp2a  10957  exple1  10961  expnlbnd2  11031  nn0ltexp2  11075  nn0leexp2  11076  expcan  11082  fiprsshashgt1  11186  fimaxq  11198  hashtpgim  11221  hashtpg  11223  fun2dmnop0  11226  ccatass  11300  swrdlen  11348  swrdfv  11349  swrdswrdlem  11400  ccatopth  11412  maxleastb  11903  maxltsup  11907  xrltmaxsup  11946  xrmaxltsup  11947  xrmaxaddlem  11949  addcn2  11999  mulcn2  12001  dvdsmodexp  12485  dvdsadd2b  12530  dvdsmod  12552  oexpneg  12567  divalglemex  12612  divalg  12614  gcdass  12715  rplpwr  12727  rppwr  12728  nnwodc  12736  coprmdvds2  12794  rpmulgcd2  12796  qredeq  12797  rpdvds  12800  cncongr2  12805  rpexp  12854  znege1  12879  prmdiveq  12937  hashgcdlem  12939  odzdvds  12947  modprmn0modprm0  12958  coprimeprodsq2  12960  pythagtriplem3  12969  pcdvdsb  13022  pcgcd1  13030  qexpz  13054  pockthg  13059  ctinf  13198  nninfdc  13221  unbendc  13222  isnsgrp  13636  issubmnd  13672  ress0g  13673  mulgneg  13874  mulgdirlem  13887  submmulg  13900  subgmulg  13922  nmzsubg  13944  ghmmulg  13990  srg1zr  14148  ring1eq0  14209  mulgass2  14219  rhmdvdsr  14337  rmodislmodlem  14515  rmodislmod  14516  lssintclm  14549  rnglidlrng  14663  2idlcpblrng  14688  neiint  15027  topssnei  15044  iscnp4  15100  cnptopco  15104  cnconst2  15115  cnrest2  15118  cnptoprest  15121  cnpdis  15124  bldisj  15283  blgt0  15284  bl2in  15285  blss2ps  15288  blss2  15289  xblm  15299  blssps  15309  blss  15310  xmetresbl  15322  bdbl  15385  metcnp3  15393  metcnp2  15395  cncfmptc  15478  dvcnp2cntop  15581  dvcn  15582  logdivlti  15763  ltexp2  15823  pellexlem2  15863  lgsfcl2  15896  lgsdilem  15917  lgsdirprm  15924  lgsdir  15925  lgsdi  15927  lgsne0  15928  incistruhgr  16102  clwwlkext2edg  16434  clwwlknonex2e  16452