Theorem syl6bi 243

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

Ref	Expression
syl6bi.1	|- ( ph -> ( ps <-> ch ) )
syl6bi.2	|- ( ch -> th )

Assertion

Ref	Expression
syl6bi	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6bi

Step	Hyp	Ref	Expression
1		syl6bi.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 219	. 2 |- ( ph -> ( ps -> ch ) )
3		syl6bi.2	. 2 |- ( ch -> th )
4	2, 3	syl6 35	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 196

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

This theorem is referenced by:  ax12i  1879  sb3  2355  2eu2  2554  reu6  3395  sseq0  3975  disjel  4023  disjpss  4028  uneqdifeqOLD  4058  preq12b  4382  prel12  4383  prneimg  4388  elinti  4485  zfrepclf  4777  dtru  4857  opth1g  4947  propeqop  4970  otsndisj  4979  otiunsndisj  4980  iunopeqop  4981  elreldm  5350  dfres3  5403  issref  5509  relcnvtr  5655  relresfld  5662  ordtr2  5768  ordssun  5827  funopg  5922  funimass2  5972  f0dom0  6089  elfv2ex  6229  fveqdmss  6354  eldmrexrnb  6366  fvcofneq  6367  funopsn  6413  funopdmsn  6415  funsndifnop  6416  elunirn  6509  2f1fvneq  6517  oprabid  6677  brfvopab  6700  limuni3  7052  peano5  7089  op1steq  7210  el2mpt2csbcl  7250  bropopvvv  7255  bropfvvvv  7257  f1o2ndf1  7285  frxp  7287  fnwelem  7292  suppimacnv  7306  fvn0elsuppb  7312  suppfnss  7320  reldmtpos  7360  rntpos  7365  seqomlem2  7546  oaordi  7626  oa00  7639  oalimcl  7640  omeulem1  7662  nnaordi  7698  ecopovtrn  7850  undifixp  7944  mapdom2  8131  unxpdomlem3  8166  enp1i  8195  findcard2  8200  infssuni  8257  wdompwdom  8483  opthreg  8515  inf3lemd  8524  inf3lem2  8526  inf3lem6  8530  cnfcomlem  8596  cnfcom3  8601  karden  8758  carden2a  8792  alephdom  8904  dfac5lem4  8949  dfac12r  8968  kmlem2  8973  kmlem12  8983  cfslb2n  9090  alephsing  9098  fin23lem30  9164  fin1a2lem6  9227  fin1a2lem13  9234  axcc2lem  9258  domtriomlem  9264  axdc3lem2  9273  axdc4lem  9277  brdom6disj  9354  alephexp1  9401  pwfseq  9486  addnidpi  9723  indpi  9729  nqereu  9751  ltsonq  9791  distrlem5pr  9849  addcanpr  9868  suplem1pr  9874  suplem2pr  9875  ltsrpr  9898  ltsosr  9915  sqgt0sr  9927  leltne  10127  ltnsym  10135  ltlen  10138  eqlei  10147  eqlei2  10148  infm3  10982  nnunb  11288  0mnnnnn0  11325  elnnnn0b  11337  nn0ge2m1nn  11360  nn0le2is012  11441  btwnz  11479  uz11  11710  zq  11794  xrleltne  11978  xltnegi  12047  xnn0lenn0nn0  12075  xnn0xadd0  12077  xmulasslem2  12112  reltxrnmnf  12172  icogelb  12225  iccleub  12229  uznfz  12423  2ffzeq  12460  elfzonlteqm1  12543  elfzo0l  12558  elfznelfzob  12574  elfzr  12581  elfzlmr  12582  injresinjlem  12588  injresinj  12589  fleqceilz  12653  modadd1  12707  modmul1  12723  modirr  12741  addmodlteq  12745  uzrdgfni  12757  fsuppmapnn0fiub0  12793  fsuppmapnn0ub  12795  seqf1o  12842  hashrabsn01  13162  hashrabsn1  13163  hash1snb  13207  hash1n0  13209  hashf1lem2  13240  hash2prde  13252  hash2prd  13257  hash2pwpr  13258  hashle2pr  13259  hashle2prv  13260  hashge2el2dif  13262  hashge2el2difr  13263  fundmge2nop0  13274  ffz0iswrd  13332  ccatrcl1  13376  2swrd1eqwrdeq  13454  wrdind  13476  wrd2ind  13477  swrdccatin1  13483  swrdccat3blem  13495  2cshwcshw  13571  cshwcsh2id  13574  cshimadifsn  13575  2swrd2eqwrdeq  13696  wwlktovf  13699  wwlktovfo  13701  s3sndisj  13706  s3iunsndisj  13707  relexpindlem  13803  rexico  14093  lo1le  14382  fsum2dlem  14501  ntrivcvg  14629  fprodss  14678  fprod2dlem  14710  0dvds  15002  mod2eq1n2dvds  15071  opoe  15087  omoe  15088  opeo  15089  omeo  15090  m1exp1  15093  nn0enne  15094  nn0o1gt2  15097  gcdneg  15243  dfgcd2  15263  algcvga  15292  eucalglt  15298  lcmf  15346  coprmdvds  15366  divgcdcoprmex  15380  cncongr1  15381  prm2orodd  15404  prm23lt5  15519  pockthi  15611  prmreclem5  15624  ramtcl2  15715  cshwrepswhash1  15809  f1ocpbl  16185  f1ovscpbl  16186  f1olecpbl  16187  monhom  16395  epihom  16402  inveq  16434  invcoisoid  16452  isocoinvid  16453  ciclcl  16462  cicrcl  16463  isinitoi  16653  istermoi  16654  2initoinv  16660  2termoinv  16667  setciso  16741  embedsetcestrclem  16797  ipopos  17160  gsumval2a  17279  ismnddef  17296  dfgrp2e  17448  symg2bas  17818  symgfix2  17836  gsmsymgreq  17852  pmtrdifellem4  17899  mndodcongi  17962  pj1eu  18109  dprd2da  18441  rimf1o  18734  rimrhm  18735  brric2  18745  lmodfopnelem1  18899  lspdisjb  19126  lspsnsubn0  19140  0ring01eq  19271  psrbaglefi  19372  obs2ss  20073  mamufacex  20195  mat0dim0  20273  mat0dimid  20274  mat0dimscm  20275  dmatmat  20300  scmatmat  20315  mat1scmat  20345  1mavmul  20354  mavmulsolcl  20357  gsummatr01  20465  cpmatpmat  20515  cpmadugsumlemF  20681  tg2  20769  tgcl  20773  neii1  20910  neii2  20912  neindisj2  20927  perfopn  20989  ordtbas2  20995  pnfnei  21024  mnfnei  21025  llyidm  21291  txlm  21451  qtopuni  21505  tgqtop  21515  isfild  21662  snfil  21668  fbunfip  21673  fgss2  21678  fmco  21765  fbflim2  21781  cnpflf2  21804  fcfelbas  21840  fcfneii  21841  alexsubALTlem2  21852  alexsubALT  21855  tgpconncompeqg  21915  tsmscl  21938  tngngpim  22463  tgioo  22599  xrsmopn  22615  iccntr  22624  reconnlem2  22630  addcnlem  22667  htpycn  22772  phtpyhtpy  22781  pi1blem  22839  fgcfil  23069  ioombl1lem4  23329  dyadmbl  23368  itg2gt0  23527  ditgneg  23621  dvivthlem1  23771  coeeq2  23998  aannenlem2  24084  sineq0  24273  efif1o  24292  leibpilem1  24667  xrlimcnp  24695  vmacl  24844  efvmacl  24846  vmalelog  24930  dchrelbasd  24964  lgsqr  25076  gausslemma2dlem0i  25089  2lgslem2  25120  2lgs  25132  2lgsoddprmlem3  25139  uhgr0vb  25967  umgrupgr  25998  umgrnloopv  26001  umgredgprv  26002  umgrislfupgrlem  26017  umgredg  26033  uspgrushgr  26070  uspgrupgr  26071  usgruspgr  26073  usgredgprvALT  26087  usgrnloopvALT  26093  uhgr2edg  26100  edg0usgr  26145  egrsubgr  26169  0uhgrsubgr  26171  uhgrspansubgrlem  26182  nbuhgr  26239  nbgrisvtx  26255  uvtxaisvtx  26289  vtxnbuvtx  26291  uvtx2vtx1edg  26299  cusgrsize2inds  26349  cusgrfilem2  26352  vtxdg0v  26369  1loopgrnb0  26398  vtxdginducedm1lem4  26438  wlkvtxeledg  26519  wlkeq  26529  wlkl1loop  26534  wlk1walk  26535  upgrwlkedg  26538  uspgr2wlkeq  26542  wlkv0  26547  wlkonl1iedg  26561  wlkon2n0  26562  wlkp1lem8  26577  wlkp1  26578  lfgrwlkprop  26584  lfgrwlknloop  26586  upgrwlkdvde  26633  spthonepeq  26648  uhgrwkspthlem2  26650  usgr2wlkneq  26652  usgr2trlncl  26656  usgr2trlspth  26657  pthdlem2lem  26663  uspgrn2crct  26700  wwlks  26727  wwlknbp  26733  0enwwlksnge1  26749  wwlkswwlksn  26750  wlklnwwlkln1  26754  wwlksnextproplem3  26806  wwlksnextprop  26807  wspthsnonn0vne  26813  2pthon3v  26839  umgr2adedgspth  26844  wwlks2onv  26847  rusgr0edg  26868  clwwlknclwwlkdifs  26873  clwwlknbp0  26884  isclwwlksnx  26889  clwwlkclwwlkn  26891  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a4  26898  clwlkclwwlklem2  26901  clwwlksext2edg  26923  erclwwlksneqlen  26945  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfclwwlk  26962  clwlksf1clwwlklem  26968  upgr1wlkdlem1  27005  upgr3v3e3cycl  27040  uhgr3cyclexlem  27041  1conngr  27054  conngrv2edg  27055  eupth2lem3lem4  27091  eulercrct  27102  frgrusgrfrcond  27123  frgr3vlem2  27138  1to2vfriswmgr  27143  1to3vfriswmgr  27144  frgrncvvdeqlem9  27171  frgrwopreg  27187  frgr2wwlkeqm  27195  2wspmdisj  27201  numclwwlkovf2exlem2  27212  numclwlk1lem2f1  27227  frgrreggt1  27251  frgrregord013  27253  frgrregord13  27254  l2p  27331  nmlno0lem  27648  normgt0  27984  ocin  28155  nmlnop0iALT  28854  nmopun  28873  cvpss  29144  cvnbtwn  29145  atcvati  29245  mdsymlem6  29267  issgon  30186  mbfmcnt  30330  ballotlemfc0  30554  ballotlemfcc  30555  mthmblem  31477  soasym  31657  sltintdifex  31814  sltres  31815  nosepnelem  31830  nolt02o  31845  pprodss4v  31991  funpartfun  32050  funpartfv  32052  5segofs  32113  btwnxfr  32163  brofs2  32184  brifs2  32185  btwnconn1  32208  segleantisym  32222  broutsideof2  32229  outsidene1  32230  outsidene2  32231  funray  32247  lineunray  32254  cldbnd  32321  bj-dtru  32797  bj-ismoored0  33061  topdifinffinlem  33195  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlpssretop  33212  matunitlindf  33407  poimir  33442  volsupnfl  33454  itg2addnclem  33461  cover2  33508  sdclem2  33538  fdc  33541  sstotbnd3  33575  heibor1  33609  clmgmOLD  33650  smgrpmgm  33663  smgrpassOLD  33664  dvrunz  33753  0rngo  33826  lsatcvat  34337  lshpkrex  34405  cmtbr3N  34541  atn0  34595  atnle  34604  cvlsupr4  34632  cvlsupr5  34633  cvlsupr6  34634  cvrval4N  34700  cvratlem  34707  2llnjN  34853  2lplnj  34906  linepsubN  35038  elpaddatiN  35091  elpcliN  35179  pclcmpatN  35187  ldilval  35399  ltrnu  35407  cdleme18d  35582  tendotp  36049  tendof  36051  tendovalco  36053  diatrl  36333  diaintclN  36347  dvheveccl  36401  dibintclN  36456  dihord6apre  36545  dihmeetlem1N  36579  dihpN  36625  dihintcl  36633  dochkrshp4  36678  pw2f1ocnv  37604  iocinico  37797  expgrowthi  38532  iotavalsb  38634  bi23imp1  38701  ioogtlb  39717  iocgtlb  39724  iocleub  39725  icoltub  39732  iooltub  39735  stoweidlem31  40248  2reu2  41187  eu2ndop1stv  41202  funressnfv  41208  afvelrnb0  41244  otiunsndisjX  41298  el1fzopredsuc  41335  fzoopth  41337  2ffzoeq  41338  iccpartimp  41353  iccpartrn  41366  iccpartf  41367  iccpartnel  41374  fargshiftf  41376  fargshiftfo  41378  pfxsuff1eqwrdeq  41407  fmtnofac1  41482  prmdvdsfmtnof1lem2  41497  31prm  41512  lighneallem3  41524  nn0o1gt2ALTV  41605  nn0oALTV  41607  odd2prm2  41627  mogoldbblem  41629  sbgoldbaltlem1  41667  nnsum3primesle9  41682  bgoldbtbndlem1  41693  bgoldbtbndlem2  41694  upwlkbprop  41719  sprel  41734  sprsymrelfvlem  41740  sprsymrelfolem2  41743  mgmpropd  41775  clcllaw  41827  intop  41839  assintop  41845  assintopcllaw  41848  rngimf1o  41905  rngimrnghm  41906  c0snmgmhm  41914  elrngchom  41968  rnghmsubcsetclem1  41975  rnghmsubcsetclem2  41976  rngcid  41979  rngcinv  41981  rngciso  41982  elrngchomALTV  41986  rngccatidALTV  41989  rngcinvALTV  41993  rngcisoALTV  41994  funcrngcsetcALT  41999  zrinitorngc  42000  zrtermorngc  42001  elringchom  42014  rhmsubcsetclem1  42021  rhmsubcsetclem2  42022  ringcid  42025  rhmsubcrngclem1  42027  rhmsubcrngclem2  42028  ringcinv  42032  ringciso  42033  funcringcsetcALTV2lem7  42042  elringchomALTV  42049  ringccatidALTV  42052  ringcinvALTV  42056  ringcisoALTV  42057  funcringcsetclem7ALTV  42065  irinitoringc  42069  zrtermoringc  42070  rhmsubclem3  42088  rhmsubclem4  42089  rhmsubcALTVlem3  42106  rhmsubcALTVlem4  42107  ztprmneprm  42125  suppmptcfin  42160  linccl  42203  linc1  42214  lincolss  42223  ldepspr  42262  nn0sumshdiglem1  42415