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  7576  enq0tr  7754  distrlem4prl  7904  distrlem4pru  7905  ltaprg  7939  aptiprlemu  7960  lelttr  8367  readdcan  8418  addcan  8458  addcan2  8459  ltadd2  8698  ltmul1a  8870  ltmul1  8871  divmulassap  8974  divmulasscomap  8975  lemul1a  9137  xrlelttr  10145  xleadd1a  10212  xlesubadd  10222  icoshftf1o  10330  lincmb01cmp  10342  lincmble  10343  iccf1o  10344  fztri3or  10379  nn0p1elfzo  10528  fzofzim  10534  ioom  10627  modqmuladdim  10736  modqm1p1mod0  10744  q2submod  10754  modqaddmulmod  10760  ltexp2a  10960  exple1  10964  expnlbnd2  11035  nn0ltexp2  11079  nn0leexp2  11080  expcan  11086  fiprsshashgt1  11190  fimaxq  11202  hashtpgim  11225  hashtpg  11227  fun2dmnop0  11230  ccatass  11304  swrdlen  11352  swrdfv  11353  swrdswrdlem  11404  ccatopth  11416  maxleastb  11907  maxltsup  11911  xrltmaxsup  11950  xrmaxltsup  11951  xrmaxaddlem  11953  addcn2  12003  mulcn2  12005  dvdsmodexp  12489  dvdsadd2b  12534  dvdsmod  12556  oexpneg  12571  divalglemex  12616  divalg  12618  gcdass  12719  rplpwr  12731  rppwr  12732  nnwodc  12740  coprmdvds2  12798  rpmulgcd2  12800  qredeq  12801  rpdvds  12804  cncongr2  12809  rpexp  12858  znege1  12883  prmdiveq  12941  hashgcdlem  12943  odzdvds  12951  modprmn0modprm0  12962  coprimeprodsq2  12964  pythagtriplem3  12973  pcdvdsb  13026  pcgcd1  13034  qexpz  13058  pockthg  13063  ctinf  13202  nninfdc  13225  unbendc  13226  isnsgrp  13640  issubmnd  13676  ress0g  13677  mulgneg  13878  mulgdirlem  13891  submmulg  13904  subgmulg  13926  nmzsubg  13948  ghmmulg  13994  srg1zr  14152  ring1eq0  14213  mulgass2  14223  rhmdvdsr  14342  rmodislmodlem  14547  rmodislmod  14548  lssintclm  14581  rnglidlrng  14695  2idlcpblrng  14720  neiint  15059  topssnei  15076  iscnp4  15132  cnptopco  15136  cnconst2  15147  cnrest2  15150  cnptoprest  15153  cnpdis  15156  bldisj  15315  blgt0  15316  bl2in  15317  blss2ps  15320  blss2  15321  xblm  15331  blssps  15341  blss  15342  xmetresbl  15354  bdbl  15417  metcnp3  15425  metcnp2  15427  cncfmptc  15510  dvcnp2cntop  15613  dvcn  15614  logdivlti  15795  ltexp2  15855  pellexlem2  15895  lgsfcl2  15928  lgsdilem  15949  lgsdirprm  15956  lgsdir  15957  lgsdi  15959  lgsne0  15960  incistruhgr  16134  clwwlkext2edg  16466  clwwlknonex2e  16484