Theorem 3simpc 1060

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Assertion

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

Proof of Theorem 3simpc

Step	Hyp	Ref	Expression
1		3anrot 1043	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
2		3simpa 1058	. 2 |- ( ( ps /\ ch /\ ph ) -> ( ps /\ ch ) )
3	1, 2	sylbi 207	1 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  simp3  1063  3adant1  1079  3adantl1  1217  3adantr1  1220  pr1eqbg  4390  fpropnf1  6524  find  7091  tz7.49c  7541  eqsup  8362  fimin2g  8403  mulcanenq  9782  elnpi  9810  divcan2  10693  diveq0  10695  divrec  10701  divcan3  10711  eliooord  12233  fzrev3  12406  modaddabs  12708  modaddmod  12709  muladdmodid  12710  modmulmod  12735  sqdiv  12928  swrdlend  13431  swrdnd  13432  ccats1swrdeqbi  13498  sqrmo  13992  muldvds2  15007  dvdscmul  15008  dvdsmulc  15009  dvdstr  15018  funcestrcsetclem9  16788  funcsetcestrclem9  16803  domneq0  19297  aspid  19330  znleval2  19904  redvr  19963  scmatscmiddistr  20314  1marepvmarrepid  20381  mat2pmatghm  20535  pmatcollpw1lem1  20579  monmatcollpw  20584  pmatcollpwscmatlem2  20595  conncompss  21236  islly2  21287  elmptrab2OLD  21631  elmptrab2  21632  tngngp3  22460  lmmcvg  23059  ivthicc  23227  aaliou3lem7  24104  logimcl  24316  qrngdiv  25313  ax5seg  25818  uhgr2edg  26100  umgr2edgneu  26106  uspgr1ewop  26140  iswlkg  26509  wlkonprop  26554  wlkonwlk  26558  trlsonprop  26604  trlontrl  26607  upgrwlkdvspth  26635  pthsonprop  26640  spthonprop  26641  pthonpth  26644  spthonpthon  26647  uhgrwkspth  26651  usgr2wlkspthlem1  26653  usgr2wlkspthlem2  26654  usgr2wlkspth  26655  2pthon3v  26839  umgr2wlk  26845  rusgrnumwwlkg  26871  clwwlksfo  26918  clwwlksnwwlkncl  26921  clwwisshclwws  26928  clwlksfclwwlk  26962  clwlksf1clwwlklem  26968  1pthond  27004  uhgr3cyclex  27042  numclwlk1lem2f1  27227  numclwlk2lem2f  27236  numclwwlk3OLD  27242  numclwwlk3  27243  ajfuni  27715  funadj  28745  fovcld  29440  trleile  29666  isinftm  29735  bnj1098  30854  bnj546  30966  bnj998  31026  bnj1006  31029  bnj1173  31070  bnj1189  31077  cgr3permute1  32155  cgr3com  32160  brifs2  32185  idinside  32191  btwnconn1  32208  lineunray  32254  wl-nfeqfb  33323  riotasv2s  34244  lsatlspsn2  34279  3dim2  34754  paddasslem14  35119  4atexlemex6  35360  cdlemg10bALTN  35924  cdlemg44  36021  tendoplcl  36069  hdmap14lem14  37173  pm13.194  38613  fmulcl  39813  fmuldfeqlem1  39814  stoweidlem17  40234  stoweidlem31  40248  dfsalgen2  40559  sigaraf  41042  sigarmf  41043  elfzelfzlble  41331  ccats1pfxeqbi  41431  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067  zlmodzxzscm  42135  divsub1dir  42307  elbigoimp  42350  digexp  42401