Theorem 3simp1 786

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp1

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

Syntax hints:   -> wi 3   /\ w3a 773

This theorem is referenced by:  3simp1i 789  3simp1d 792  syl3dan3 868  3anandis 917  3anandirs 918  limord 3018  ordunel 3074  nlimsucg 3102  omwordri 4187  oewordri 4203  oeordsuc 4205  abfii2 4536  subdit 5399  divrec2t 5703  div12t 5707  divdiv23t 5748  ltdivmult 5819  ledivmult 5820  lemuldivt 5824  ltdiv23t 5840  lediv23t 5841  xrltmint 5862  lemint 5869  nnleltp1t 5901  suprub 6003  gtndivt 6140  elioo4g 6318  lbicc2t 6337  eluz2t 6353  eluzel2 6356  peano2uz 6379  eluzfz1t 6419  fzrev3t 6446  fzrevral2t 6452  seqzm1 6481  expsubt 6529  expordit 6531  exple1t 6538  expubndt 6539  expnbndt 6585  ser1absdif 6867  bccmplt 6900  fsumcmp 6978  climsub 7066  climcmplem 7073  iserzcmp 7078  isummulc1ALT 7148  acdc2lem2 7431  acdc5lem2 7434  clsss 7629  clsndisj 7648  neiss 7664  cnco 7707  cnpco 7708  bl2in 7783  opni3 7806  methausi 7820  caun0 7880  lmfss 7883  lmuni 7886  lmle 7895  xpcn 7910  iscms2lem3 7925  bcthlem9 7941  grpinvop 8015  grpdivdiv 8022  grpmuldivass 8023  grppncan 8025  grpnpcan 8026  grppnpcan2 8027  abldivdiv4 8046  ablnnncan 8048  ablnnncan1 8050  ringass 8085  nvvcop 8151  nvmdi 8210  nvmul0or 8212  nvpncan2 8216  nvaddsub4 8221  nvnncan 8223  nvdif 8232  nvpi 8233  nvz 8236  nvabs 8240  nv1 8243  imsmetlem 8261  ipval2lem2 8288  4ipval2 8292  ipval2lem5 8294  sspba 8320  sspg 8321  nmblore 8378  isblo3i 8392  ipassr 8437  psrel 8572  psasym 8576  efifolem5 8641  shlej1t 9270  pjspansnt 9417  hoadddit 9646  kbmult 9795  kbass2t 9962  leopmul2it 9980  hstclt 10054  mdslmd4 10168  atexcht 10216  atcvatlem 10220  cdj3lem2 10267  cdj3lem2a 10268  clsrebb 10380  truni1 10386  hmeogrp 10425  efilcp 10445  fgsb2 10449  efilcp2 10450  cnfilca 10451  mslb1 10473  msra3 10475  ishomc 10561  cmpassoh 10573  imonclem 10583  ismonc 10584  cmpmon 10585  icmpmon 10587  idmon 10588

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 775

Copyright terms: Public domain