Theorem 3simp1 800

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp1

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

Syntax hints:   -> wi 3   /\ w3a 787

This theorem is referenced by:  3simp1i 803  3simp1d 806  syld3an3 882  3anandis 932  3anandirs 933  limord 3085  ordunel 3141  nlimsucg 3169  omwordri 4261  oewordri 4277  oeordsuc 4279  abfii2 4622  supmax 4649  subdi 5492  divrec2 5802  div12 5807  divdiv23 5850  ltdivmulOLD 5926  ledivmulOLD 5928  lemuldiv 5934  lemuldivOLD 5935  ltdiv23 5952  lediv23 5953  xrltmin 5974  lemin 5981  nnleltp1 6015  suprub 6138  gtndiv 6278  elioo4g 6410  lbicc2 6430  eluz2 6447  eluzel2 6450  peano2uz 6473  eluzfz1 6513  fzrev3 6540  fzrevral2 6546  seqzm1 6638  expsub 6687  expordi 6689  exple1 6696  expubnd 6697  expnbnd 6743  mulre 6867  ser1absdifi 7020  bccmpl 7052  fsumcmp 7130  climsub 7220  climcmplem 7227  iserzcmp 7232  isummulc1iALT 7303  acdc2lem2 7581  acdc5lem2 7584  clsss 7772  clsndisj 7791  neiss 7808  cnco 7853  cnpco 7854  bl2in 7928  opni3 7951  methausi 7966  caun0 8030  lmfss 8033  lmuni 8036  lmle 8045  xpcn 8061  iscms2lem3 8076  bcthlem9 8092  grpinvop 8164  grpdivdiv 8171  grpmuldivass 8172  grppncan 8174  grpnpcan 8175  grppnpcan2 8176  abldivdiv4 8193  ablnnncan 8195  ablnnncan1 8197  ringass 8232  nvvcop 8297  nvmdi 8354  nvmul0or 8356  nvpncan2 8360  nvaddsub4 8365  nvnncan 8367  nvdif 8377  nvpi 8378  nvz 8381  nvabs 8385  nv1 8388  imsmetlem 8407  ipval2lem2 8438  4ipval2 8442  ipval2lem5 8444  sspba 8470  sspg 8471  nmblore 8530  isblo3i 8545  ipassr 8590  psrel 8730  psasym 8735  pstr 8736  efifolem5 8809  shlej1 9438  pjspansn 9583  hoadddi 9812  kbmul 9962  kbass2 10133  leopmul2i 10151  hstcl 10228  mdslmd4i 10344  atexch 10392  atcvatlem 10396  cdj3lem2 10446  cdj3lem2a 10447  inposet 10578  clsrebb 10587  truni1 10593  hmeogrp 10632  hmeobc 10636  homindlem3 10645  efilcp 10664  fgsb2 10668  efilcp2 10669  cnfilca 10670  mslb1 10711  msra3 10713  ishomc 10799  cmpassoh 10811  imonclem 10823  ismonc 10824  cmpmon 10825  icmpmon 10826  idmon 10827  isepic 10834

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 154  df-an 232  df-3an 789

Copyright terms: Public domain