Theorem simpl1 1005

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

Assertion

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

Proof of Theorem simpl1

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

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

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 985

This theorem is referenced by:  simpll1  1041  simprl1  1047  simp1l1  1095  simp2l1  1101  simp3l1  1107  3anandirs  1363  rspc3ev  2904  brcogw  4868  cocan1  5884  oawordi  6585  nnmord  6633  nnmword  6634  dif1en  7009  ac6sfi  7028  ordiso2  7170  difinfsn  7235  ctssdc  7248  2omotaplemap  7411  enq0tr  7589  distrlem4prl  7739  distrlem4pru  7740  ltaprg  7774  aptiprlemu  7795  lelttr  8203  readdcan  8254  addcan  8294  addcan2  8295  ltadd2  8534  ltmul1a  8706  ltmul1  8707  divmulassap  8810  divmulasscomap  8811  lemul1a  8973  xrlelttr  9970  xleadd1a  10037  xlesubadd  10047  icoshftf1o  10155  lincmb01cmp  10167  iccf1o  10168  fztri3or  10203  fzofzim  10356  ioom  10447  modqmuladdim  10556  modqm1p1mod0  10564  q2submod  10574  modqaddmulmod  10580  ltexp2a  10780  exple1  10784  expnlbnd2  10854  nn0ltexp2  10898  nn0leexp2  10899  expcan  10905  fiprsshashgt1  11006  fimaxq  11016  fun2dmnop0  11036  ccatass  11109  swrdlen  11150  swrdfv  11151  swrdswrdlem  11202  ccatopth  11214  maxleastb  11691  maxltsup  11695  xrltmaxsup  11734  xrmaxltsup  11735  xrmaxaddlem  11737  addcn2  11787  mulcn2  11789  dvdsmodexp  12272  dvdsadd2b  12317  dvdsmod  12339  oexpneg  12354  divalglemex  12399  divalg  12401  gcdass  12502  rplpwr  12514  rppwr  12515  nnwodc  12523  coprmdvds2  12581  rpmulgcd2  12583  qredeq  12584  rpdvds  12587  cncongr2  12592  rpexp  12641  znege1  12666  prmdiveq  12724  hashgcdlem  12726  odzdvds  12734  modprmn0modprm0  12745  coprimeprodsq2  12747  pythagtriplem3  12756  pcdvdsb  12809  pcgcd1  12817  qexpz  12841  pockthg  12846  ctinf  12967  nninfdc  12990  unbendc  12991  isnsgrp  13405  issubmnd  13441  ress0g  13442  mulgneg  13643  mulgdirlem  13656  submmulg  13669  subgmulg  13691  nmzsubg  13713  ghmmulg  13759  srg1zr  13916  ring1eq0  13977  mulgass2  13987  rhmdvdsr  14104  rmodislmodlem  14279  rmodislmod  14280  lssintclm  14313  rnglidlrng  14427  2idlcpblrng  14452  neiint  14784  topssnei  14801  iscnp4  14857  cnptopco  14861  cnconst2  14872  cnrest2  14875  cnptoprest  14878  cnpdis  14881  bldisj  15040  blgt0  15041  bl2in  15042  blss2ps  15045  blss2  15046  xblm  15056  blssps  15066  blss  15067  xmetresbl  15079  bdbl  15142  metcnp3  15150  metcnp2  15152  cncfmptc  15235  dvcnp2cntop  15338  dvcn  15339  logdivlti  15520  ltexp2  15580  lgsfcl2  15650  lgsdilem  15671  lgsdirprm  15678  lgsdir  15679  lgsdi  15681  lgsne0  15682  incistruhgr  15855