Theorem syl6bb 595

Description: A syllogism inference from two biconditionals.

Hypotheses

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

Assertion

Ref	Expression
syl6bb	|- (ph -> (ps <-> th))

Proof of Theorem syl6bb

Step	Hyp	Ref	Expression
1		syl6bb.1	. 2 |- (ph -> (ps <-> ch))
2		syl6bb.2	. . 3 |- (ch <-> th)
3	2	a1i 8	. 2 |- (ph -> (ch <-> th))
4	1, 3	bitrd 587	1 |- (ph -> (ps <-> th))

Syntax hints:   -> wi 3   <-> wb 163

This theorem is referenced by:  syl6rbb 596  syl6bbr 597  3bitr3g 613  biantrurdOLD 797  19.17 1396  19.33bOLD 1445  2eu6 1858  abeq2d 2003  necon2bbid 2066  cbvralf 2276  cbvrexf 2277  cbvreuv 2282  eqvincOLD 2388  cbvrab 2421  eueq3 2430  reu7 2447  reu8 2448  sbcralt 2527  sbcralgf 2529  uniiunlem 2693  reldisjOLD 2917  sbcsngOLD 3087  prssg 3140  eqsn 3143  eluniab 3189  elintab 3227  ssintab 3233  dfiun2g 3283  dfiun2gOLD 3284  dfiin2g 3286  cbvopab1 3405  axsep2 3439  notzfaus 3478  moabex 3513  opcom 3547  opeqsn 3549  sotrieq2 3618  ordtri2 3696  ordtri4OLD 3700  oneqmini 3714  ordtri2orOLD 3767  eufromeq3 3830  eufromeq6 3833  reuxfrd 3846  elpwunsn 3856  ralxp 4041  relop 4113  opelco2g 4133  opelcnvgOLD 4141  reldm0 4176  relrn0 4204  issOLD 4255  asymref2 4310  asymref2OLD 4311  xpnz 4335  xpcan 4348  xpcan2 4350  dmsnopOLD 4368  fncnv 4479  fvprc 4678  nfunsnOLD 4707  fnopfvb 4713  funopfvb 4715  fvelrnb 4719  funimass4 4722  dffv2 4734  fvopab3 4740  fvopabn 4749  eqfnfv2OLD 4768  eqfnfv3 4769  eqfnfv2f 4770  eufnfv 4771  fvreseq 4772  elrnopabg 4773  fsn 4807  fconstfv 4825  funiunfv 4842  dff13 4850  f1ocnvfv3 4859  isocnv 4873  isoini 4877  f1oiso 4881  eloprabg 4936  resoprab 4938  eqfnoprv 4945  oprabval6g 4962  oprvelrn 4969  caoprord2 4990  cbvmpt 5011  elopabi 5059  eloprabi 5060  elrnoprabg 5066  oevn0 5199  om00el 5255  omordlim 5256  omlimcl 5257  oeoa 5272  oeoe 5274  ecopoprsym 5369  th3qlem1 5373  dom2d 5463  mapsnen 5488  undom 5497  xpdom2 5501  pw2en 5505  ac6sfilem3 5508  0sdomg 5529  fodomr 5547  mapdom2 5588  mapxpen 5589  xpmapenlem5 5594  unfilem1 5641  abfii4 5654  fodomfi 5656  inf3lem1 5719  r1tr 5765  rankval2 5781  rankr1 5785  rankval3 5792  unbndrank 5794  r1pwcl 5798  trsbc 5843  bnd2 5854  omsublim 5887  aceq0 5892  aceq5lem4 5900  aceq5 5902  zfac 5907  ac6lem 5916  kmlem14 5940  iscard2 6006  alephord2 6024  cardaleph 6033  zfcndac 6123  ltexpi 6181  mulcmpblnq 6205  ordpipq 6208  ltsopq 6227  genpelv 6255  genpprecl 6256  genpnnp 6260  genpass 6264  distrlem1pr 6279  distrlem5pr 6283  prlem936a 6305  addcmpblnr 6333  ltsrpr 6338  ltsosr 6355  mulgt0sr 6366  map2psrpr 6372  ltresr 6410  axrnegex 6436  axrrecex 6437  pre-axltadd 6442  pre-axmulgt0 6443  negcon1 6570  negcon2 6571  xrrebnd 6743  lt0neg1 6857  lt0neg2 6858  le0neg1 6859  le0neg2 6860  divmul2 6897  reclt1 7081  recgt1 7082  addltmul 7229  infm3 7263  arch 7280  supxrbnd 7300  nn0ltp1le 7336  elznn0 7358  elnnz1 7364  elnn0nn 7380  zltp1le 7390  recnz 7403  dfuzi 7414  uzindOLD 7420  uzwo3lem2 7430  iooin 7539  elioo1 7545  elioo2 7546  elioo3g 7547  elioc1 7548  elico1 7549  elicc1 7550  elioo4g 7553  iooneg 7575  iccneg 7576  icounlem 7581  snunioolem 7583  ioojoin 7585  eluz1 7589  raluz 7611  rexuz 7613  elfz1 7640  elfz2 7642  elfzuzb 7646  elfzuz2 7656  elfz2nn0 7667  fzsuc 7678  fzpr 7685  fznn0 7694  fznn 7695  seq1lem2 7723  exple1 7852  bernneq 7898  bernneqOLD 7899  sqr2irrlem3 7976  crulem 7986  creur 7992  creui 7993  abssubne0 8134  cvg2i 8174  dffsum 8258  fsumrev 8289  fsumshft 8291  clm1i 8337  clmnnsi 8344  climshfti 8364  climresi 8365  caucvgi 8423  caucvg3 8428  dfisum 8452  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  xpnnen 8768  infxpidmlem5 8825  infxpidmlem10 8830  istop2g 8866  isbasis2g 8881  isbasis3g 8882  eltg3 8896  tgss3 8908  elcls 8980  ntreq0 8984  islp 9020  islp2 9023  islpi 9025  cncnplem3 9053  cncnplem4 9054  ismet 9075  elbl 9115  blrn2 9119  blss 9130  metcnplem 9164  cncfmet 9183  dscmet 9196  lmbr2 9207  iscau2 9215  iscau5 9219  lmbrnns 9220  iscaunns 9222  metcn4 9249  isgrp 9321  issubg 9425  nvsubadd 9607  sspval 9721  isssp 9722  islno 9753  nmogtmnf 9772  nmounbi 9778  isblo 9782  ishmo 9811  ubthlem1 9872  spwmo 9999  pilem1 10020  sincosq1sgn 10053  sincosq2sgn 10054  efghgrpilem 10073  efif1lem5 10088  axgroth2 10133  grothomex 10136  axgroth6 10137  uptx 10226  isfbas2 10263  fbunfip 10282  isfillim 10298  isexid 10364  ismgm 10367  hvmulcan2 10573  hire 10593  ocel 10787  ocsh 10789  chocunii 10805  shsel 10911  shscom 10916  shmodsi 10995  elspani 11099  adjsym 11396  eigorthi 11400  nmopgtmnf 11432  adjval2 11452  cnvadj 11453  hhlnoi 11463  elnlfn 11489  eleigvec 11518  nmop0h 11553  largei 11839  mdbr2 11868  mddmd2 11881  mdsl2i 11894  chrelat3 11943  atnem0 11949  irredlem1 11962  sumdmdii 11987  sumdmdlem 11990  dmdbr5ati 11994  cdjreui 12004  bnj205 12498  bnj1171 13439  bnj1253 13470  bnj1283 13476  imim21b 13597  nn0lt10b 13603  elfzm1b 13606  fz1eqblem 13608  zmodid2 13614  elgiso 13639  alzdvds 13695  divalglem4 13699  divalgb 13707  divalgmod 13709  gcddvds 13722  zgt1b2 13772  isprm3 13776  coprm 13782  dfon2lem7 13855  dfon2 13858  predreseq 13890  xporderlem 13948  poxp 13949  soxp 13950  wfrlem1 13957  sltval2 13997  sltintdifex 14004  axfelem8 14038  axfelem9 14039  axfelem11 14041  axfelem12 14042  axfelem15 14045  axfelem16 14046  uninqs 14340  elo 14342  eloi 14400  celsor 14443  iscst4 14522  puub2 14600  puub 14601  ismxl2 14609  ismnl2 14610  dffprod 14670  vecval1b 14794  svli2 14826  sbtpsines 14905  cnfilca 14927  rcfpfillem3 14930  rcfpfillem6 14933  plimfil 14940  altretoplem1 14995  supexr 15043  ishomc 15138  ismona 15158  btmp 15252  tartarmap 15265  dfiin2gOLD 15356  fictb 15371  omsublimOLD 15396  compsublem 15430  compfipin0 15436  is1stc3 15469  isfne2 15481  isfne3 15482  comppfsc 15517  neibastop3 15524  ist0-2 15539  fbasfip 15556  flimfcn 15603  isfclus 15606  fcluscn 15619  fclsfcn 15632  euuni2 15663  unirep 15664  inpreima 15682  respreima 15684  eqfnoprv2 15704  f1opr 15714  eqfnfv3OLD 15721  fimax 15746  ac6gf 15749  indexa 15753  zornn0 15764  frfi 15771  fimaxre 15774  elfzp12 15795  fzm1 15796  sdc 15811  fdc 15812  fsum00 15820  iccshftr 15857  iccshftl 15859  iccdil 15861  icccntr 15863  heiborlem8 15962  heiborlem15 15969  rrncms 16019  rrntotbndlem1 16020  rrntotbnd 16022  isphtpy 16048  pcoass 16085  elpi1 16089  isrnghom 16119  isrngiso 16132  iscring2 16146  isidl 16162  ispridl 16182  pridlidl 16183  pridlnr 16184  pridl 16185  ismaxidl 16188  maxidlidl 16189  smprngpr 16200  prnc 16215  brabsb2 16253  prtlem13 16271  prtlem16 16272  prtlem18 16279  prter1 16282  prter3 16286  ishgrag 16291  iotasbc2 16384  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414  cbviotaf 16432  elstrdiff 16720  pleval2 16785  latnle 16880  cvrval2 16991  cvrnbtwn2 16992  cvrnbtwn3 16993  isatom 17001  leatom 17005  ps2 17079  isringNEW 17142  iscsubsp 17209  isline 17220  ispoint 17223  ispsubsp 17226  pointpsub 17231  linepsub 17232  elpmap 17238  elpadd 17260  paddcom 17274  pmapjoin 17313  pmapjat 17314  ispsubcl 17347  iswatom 17394  ispaut 17396  isdil 17403  istrn 17406

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 164  df-an 242

Copyright terms: Public domain