Theorem simpl1 1031

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

Assertion

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

Proof of Theorem simpl1

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

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

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 1011

This theorem is referenced by:  simpll1  1067  simprl1  1073  simp1l1  1121  simp2l1  1127  simp3l1  1133  3anandirs  1389  rspc3ev  2947  brcogw  4947  cocan1  5987  oawordi  6736  nnmord  6784  nnmword  6785  mapunen  7145  dif1en  7177  ac6sfi  7196  ordiso2  7369  difinfsn  7434  ctssdc  7447  2omotaplemap  7617  enq0tr  7795  distrlem4prl  7945  distrlem4pru  7946  ltaprg  7980  aptiprlemu  8001  lelttr  8408  readdcan  8460  addcan  8500  addcan2  8501  ltadd2  8741  ltmul1a  8913  ltmul1  8914  divmulassap  9019  divmulasscomap  9020  lemul1a  9182  xrlelttr  10191  xleadd1a  10258  xlesubadd  10268  icoshftf1o  10376  lincmb01cmp  10388  lincmble  10389  iccf1o  10390  fztri3or  10426  nn0p1elfzo  10577  fzofzim  10583  ioom  10678  modqmuladdim  10787  modqm1p1mod0  10795  q2submod  10805  modqaddmulmod  10811  ltexp2a  11011  exple1  11015  expnlbnd2  11086  nn0ltexp2  11130  nn0leexp2  11131  expcan  11137  fiprsshashgt1  11241  fimaxq  11253  hashtpgim  11280  hashtpg  11282  fun2dmnop0  11285  ccatass  11359  swrdlen  11407  swrdfv  11408  swrdswrdlem  11459  ccatopth  11471  maxleastb  11963  maxltsup  11967  xrltmaxsup  12006  xrmaxltsup  12007  xrmaxaddlem  12009  addcn2  12059  mulcn2  12061  dvdsmodexp  12545  dvdsadd2b  12590  dvdsmod  12612  oexpneg  12627  divalglemex  12672  divalg  12674  gcdass  12775  rplpwr  12787  rppwr  12788  nnwodc  12796  coprmdvds2  12854  rpmulgcd2  12856  qredeq  12857  rpdvds  12860  cncongr2  12865  rpexp  12914  znege1  12939  prmdiveq  12997  hashgcdlem  12999  odzdvds  13007  modprmn0modprm0  13018  coprimeprodsq2  13020  pythagtriplem3  13029  pcdvdsb  13082  pcgcd1  13090  qexpz  13114  pockthg  13119  ctinf  13304  nninfdc  13327  unbendc  13328  isnsgrp  13704  issubmnd  13738  ress0g  13739  mulgneg  13926  mulgdirlem  13939  submmulg  13952  subgmulg  13974  nmzsubg  13996  ghmmulg  14042  ring1eq0  14336  mulgass2  14346  rhmdvdsr  14465  rmodislmodlem  14670  rmodislmod  14671  lssintclm  14704  rnglidlrng  14818  2idlcpblrng  14843  issubassa  14996  neiint  15229  topssnei  15246  iscnp4  15302  cnptopco  15306  cnconst2  15317  cnrest2  15320  cnptoprest  15323  cnpdis  15326  bldisj  15485  blgt0  15486  bl2in  15487  blss2ps  15490  blss2  15491  xblm  15501  blssps  15511  blss  15512  xmetresbl  15524  bdbl  15587  metcnp3  15595  metcnp2  15597  cncfmptc  15680  dvcnp2cntop  15783  dvcn  15784  logdivlti  15965  ltexp2  16026  pellexlem2  16075  lgsfcl2  16108  lgsdilem  16129  lgsdirprm  16136  lgsdir  16137  lgsdi  16139  lgsne0  16140  incistruhgr  16314  clwwlkext2edg  16646  clwwlknonex2e  16664