Theorem simpl1 1026

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

Assertion

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

Proof of Theorem simpl1

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

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

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 1006

This theorem is referenced by:  simpll1  1062  simprl1  1068  simp1l1  1116  simp2l1  1122  simp3l1  1128  3anandirs  1384  rspc3ev  2926  brcogw  4901  cocan1  5933  oawordi  6642  nnmord  6690  nnmword  6691  dif1en  7073  ac6sfi  7092  ordiso2  7239  difinfsn  7304  ctssdc  7317  2omotaplemap  7481  enq0tr  7659  distrlem4prl  7809  distrlem4pru  7810  ltaprg  7844  aptiprlemu  7865  lelttr  8273  readdcan  8324  addcan  8364  addcan2  8365  ltadd2  8604  ltmul1a  8776  ltmul1  8777  divmulassap  8880  divmulasscomap  8881  lemul1a  9043  xrlelttr  10046  xleadd1a  10113  xlesubadd  10123  icoshftf1o  10231  lincmb01cmp  10243  iccf1o  10244  fztri3or  10279  nn0p1elfzo  10427  fzofzim  10433  ioom  10526  modqmuladdim  10635  modqm1p1mod0  10643  q2submod  10653  modqaddmulmod  10659  ltexp2a  10859  exple1  10863  expnlbnd2  10933  nn0ltexp2  10977  nn0leexp2  10978  expcan  10984  fiprsshashgt1  11087  fimaxq  11097  hashtpgim  11115  hashtpg  11117  fun2dmnop0  11120  ccatass  11194  swrdlen  11242  swrdfv  11243  swrdswrdlem  11294  ccatopth  11306  maxleastb  11797  maxltsup  11801  xrltmaxsup  11840  xrmaxltsup  11841  xrmaxaddlem  11843  addcn2  11893  mulcn2  11895  dvdsmodexp  12379  dvdsadd2b  12424  dvdsmod  12446  oexpneg  12461  divalglemex  12506  divalg  12508  gcdass  12609  rplpwr  12621  rppwr  12622  nnwodc  12630  coprmdvds2  12688  rpmulgcd2  12690  qredeq  12691  rpdvds  12694  cncongr2  12699  rpexp  12748  znege1  12773  prmdiveq  12831  hashgcdlem  12833  odzdvds  12841  modprmn0modprm0  12852  coprimeprodsq2  12854  pythagtriplem3  12863  pcdvdsb  12916  pcgcd1  12924  qexpz  12948  pockthg  12953  ctinf  13074  nninfdc  13097  unbendc  13098  isnsgrp  13512  issubmnd  13548  ress0g  13549  mulgneg  13750  mulgdirlem  13763  submmulg  13776  subgmulg  13798  nmzsubg  13820  ghmmulg  13866  srg1zr  14024  ring1eq0  14085  mulgass2  14095  rhmdvdsr  14213  rmodislmodlem  14388  rmodislmod  14389  lssintclm  14422  rnglidlrng  14536  2idlcpblrng  14561  neiint  14898  topssnei  14915  iscnp4  14971  cnptopco  14975  cnconst2  14986  cnrest2  14989  cnptoprest  14992  cnpdis  14995  bldisj  15154  blgt0  15155  bl2in  15156  blss2ps  15159  blss2  15160  xblm  15170  blssps  15180  blss  15181  xmetresbl  15193  bdbl  15256  metcnp3  15264  metcnp2  15266  cncfmptc  15349  dvcnp2cntop  15452  dvcn  15453  logdivlti  15634  ltexp2  15694  lgsfcl2  15764  lgsdilem  15785  lgsdirprm  15792  lgsdir  15793  lgsdi  15795  lgsne0  15796  incistruhgr  15970  clwwlkext2edg  16302  clwwlknonex2e  16320