Theorem simpl1 990

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

Assertion

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

Proof of Theorem simpl1

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simpll1  1026  simprl1  1032  simp1l1  1080  simp2l1  1086  simp3l1  1092  3anandirs  1338  rspc3ev  2847  brcogw  4773  cocan1  5755  oawordi  6437  nnmord  6485  nnmword  6486  dif1en  6845  ac6sfi  6864  ordiso2  7000  difinfsn  7065  ctssdc  7078  enq0tr  7375  distrlem4prl  7525  distrlem4pru  7526  ltaprg  7560  aptiprlemu  7581  lelttr  7987  readdcan  8038  addcan  8078  addcan2  8079  ltadd2  8317  ltmul1a  8489  ltmul1  8490  divmulassap  8591  divmulasscomap  8592  lemul1a  8753  xrlelttr  9742  xleadd1a  9809  xlesubadd  9819  icoshftf1o  9927  lincmb01cmp  9939  iccf1o  9940  fztri3or  9974  fzofzim  10123  ioom  10196  modqmuladdim  10302  modqm1p1mod0  10310  q2submod  10320  modqaddmulmod  10326  ltexp2a  10507  exple1  10511  expnlbnd2  10580  nn0ltexp2  10623  nn0leexp2  10624  expcan  10629  fiprsshashgt1  10730  fimaxq  10740  maxleastb  11156  maxltsup  11160  xrltmaxsup  11198  xrmaxltsup  11199  xrmaxaddlem  11201  addcn2  11251  mulcn2  11253  dvdsmodexp  11735  dvdsadd2b  11780  dvdsmod  11800  oexpneg  11814  divalglemex  11859  divalg  11861  gcdass  11948  rplpwr  11960  rppwr  11961  nnwodc  11969  coprmdvds2  12025  rpmulgcd2  12027  qredeq  12028  rpdvds  12031  cncongr2  12036  rpexp  12085  znege1  12110  prmdiveq  12168  hashgcdlem  12170  odzdvds  12177  modprmn0modprm0  12188  coprimeprodsq2  12190  pythagtriplem3  12199  pcdvdsb  12251  pcgcd1  12259  qexpz  12282  pockthg  12287  ctinf  12363  nninfdc  12386  unbendc  12387  neiint  12785  topssnei  12802  iscnp4  12858  cnptopco  12862  cnconst2  12873  cnrest2  12876  cnptoprest  12879  cnpdis  12882  bldisj  13041  blgt0  13042  bl2in  13043  blss2ps  13046  blss2  13047  xblm  13057  blssps  13067  blss  13068  xmetresbl  13080  bdbl  13143  metcnp3  13151  metcnp2  13153  cncfmptc  13222  dvcnp2cntop  13303  dvcn  13304  logdivlti  13442  ltexp2  13500  lgsfcl2  13547  lgsdilem  13568  lgsdirprm  13575  lgsdir  13576  lgsdi  13578  lgsne0  13579