Theorem 3simp1 788

Description: Simplification of triple conjunction.

Assertion

Ref	Expression
3simp1	|- ((ph /\ ps /\ ch) -> ph)

Proof of Theorem 3simp1

Step	Hyp	Ref	Expression
1		3simpa 785	. 2 |- ((ph /\ ps /\ ch) -> (ph /\ ps))
2	1	pm3.26d 321	1 |- ((ph /\ ps /\ ch) -> ph)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  3simp1i 791  3simp1d 794  syld3an3 870  3anandis 920  3anandirs 921  limord 3028  ordunel 3084  nlimsucg 3112  omwordri 4203  oewordri 4219  oeordsuc 4221  abfii2OLD 4562  supmax 4589  subdit 5427  divrec2t 5740  div12t 5744  divdiv23t 5792  ltdivmultOLD 5868  ledivmultOLD 5869  lemuldivt 5874  lemuldivtOLD 5875  ltdiv23t 5892  lediv23t 5893  xrltmint 5914  lemint 5921  nnleltp1t 5954  suprub 6056  gtndivt 6193  elioo4g 6385  lbicc2t 6404  eluz2t 6421  eluzel2 6424  peano2uz 6447  eluzfz1t 6487  fzrev3t 6514  fzrevral2t 6520  seqzm1 6549  expsubt 6598  expordit 6600  exple1t 6607  expubndt 6608  expnbndt 6654  mulretOLD 6777  ser1absdif 6930  bccmplt 6962  fsumcmp 7040  climsub 7130  climcmplem 7137  iserzcmp 7142  isummulc1ALT 7213  acdc2lem2 7489  acdc5lem2 7492  clsss 7687  clsndisj 7706  neiss 7723  cnco 7768  cnpco 7769  bl2in 7843  opni3 7866  methausi 7881  caun0 7945  lmfss 7948  lmuni 7951  lmle 7960  xpcn 7976  iscms2lem3 7991  bcthlem9 8007  grpinvop 8080  grpdivdiv 8087  grpmuldivass 8088  grppncan 8090  grpnpcan 8091  grppnpcan2 8092  abldivdiv4 8109  ablnnncan 8111  ablnnncan1 8113  ringass 8148  nvvcop 8213  nvmdi 8270  nvmul0or 8272  nvpncan2 8276  nvaddsub4 8281  nvnncan 8283  nvdif 8293  nvpi 8294  nvz 8297  nvabs 8301  nv1 8304  imsmetlem 8323  ipval2lem2 8354  4ipval2 8358  ipval2lem5 8360  sspba 8386  sspg 8387  nmblore 8446  isblo3i 8461  ipassr 8506  psrel 8646  psasym 8651  pstr 8652  efifolem5 8726  shlej1t 9355  pjspansnt 9500  hoadddit 9729  kbmult 9879  kbass2t 10050  leopmul2it 10068  hstclt 10144  mdslmd4 10260  atexcht 10308  atcvatlem 10312  cdj3lem2 10362  cdj3lem2a 10363  clsrebb 10493  truni1 10499  hmeogrp 10538  hmeobc 10542  homindlem3 10551  efilcp 10572  efilcpOLD 10573  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  mslb1 10629  msra3 10631  ishomc 10717  cmpassoh 10729  imonclem 10741  ismonc 10742  cmpmon 10743  icmpmon 10744  idmon 10745

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain