Theorem simpl1 1024

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

Assertion

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

Proof of Theorem simpl1

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

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

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 1004

This theorem is referenced by:  simpll1  1060  simprl1  1066  simp1l1  1114  simp2l1  1120  simp3l1  1126  3anandirs  1382  rspc3ev  2924  brcogw  4891  cocan1  5917  oawordi  6623  nnmord  6671  nnmword  6672  dif1en  7049  ac6sfi  7068  ordiso2  7210  difinfsn  7275  ctssdc  7288  2omotaplemap  7451  enq0tr  7629  distrlem4prl  7779  distrlem4pru  7780  ltaprg  7814  aptiprlemu  7835  lelttr  8243  readdcan  8294  addcan  8334  addcan2  8335  ltadd2  8574  ltmul1a  8746  ltmul1  8747  divmulassap  8850  divmulasscomap  8851  lemul1a  9013  xrlelttr  10010  xleadd1a  10077  xlesubadd  10087  icoshftf1o  10195  lincmb01cmp  10207  iccf1o  10208  fztri3or  10243  fzofzim  10396  ioom  10488  modqmuladdim  10597  modqm1p1mod0  10605  q2submod  10615  modqaddmulmod  10621  ltexp2a  10821  exple1  10825  expnlbnd2  10895  nn0ltexp2  10939  nn0leexp2  10940  expcan  10946  fiprsshashgt1  11047  fimaxq  11057  fun2dmnop0  11077  ccatass  11151  swrdlen  11192  swrdfv  11193  swrdswrdlem  11244  ccatopth  11256  maxleastb  11733  maxltsup  11737  xrltmaxsup  11776  xrmaxltsup  11777  xrmaxaddlem  11779  addcn2  11829  mulcn2  11831  dvdsmodexp  12314  dvdsadd2b  12359  dvdsmod  12381  oexpneg  12396  divalglemex  12441  divalg  12443  gcdass  12544  rplpwr  12556  rppwr  12557  nnwodc  12565  coprmdvds2  12623  rpmulgcd2  12625  qredeq  12626  rpdvds  12629  cncongr2  12634  rpexp  12683  znege1  12708  prmdiveq  12766  hashgcdlem  12768  odzdvds  12776  modprmn0modprm0  12787  coprimeprodsq2  12789  pythagtriplem3  12798  pcdvdsb  12851  pcgcd1  12859  qexpz  12883  pockthg  12888  ctinf  13009  nninfdc  13032  unbendc  13033  isnsgrp  13447  issubmnd  13483  ress0g  13484  mulgneg  13685  mulgdirlem  13698  submmulg  13711  subgmulg  13733  nmzsubg  13755  ghmmulg  13801  srg1zr  13958  ring1eq0  14019  mulgass2  14029  rhmdvdsr  14147  rmodislmodlem  14322  rmodislmod  14323  lssintclm  14356  rnglidlrng  14470  2idlcpblrng  14495  neiint  14827  topssnei  14844  iscnp4  14900  cnptopco  14904  cnconst2  14915  cnrest2  14918  cnptoprest  14921  cnpdis  14924  bldisj  15083  blgt0  15084  bl2in  15085  blss2ps  15088  blss2  15089  xblm  15099  blssps  15109  blss  15110  xmetresbl  15122  bdbl  15185  metcnp3  15193  metcnp2  15195  cncfmptc  15278  dvcnp2cntop  15381  dvcn  15382  logdivlti  15563  ltexp2  15623  lgsfcl2  15693  lgsdilem  15714  lgsdirprm  15721  lgsdir  15722  lgsdi  15724  lgsne0  15725  incistruhgr  15898