Theorem 3bitri 194

Description: A chained inference from transitive law for logical equivalence.

Hypotheses

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

Assertion

Ref	Expression
3bitri	|- (ph <-> th)

Proof of Theorem 3bitri

Step	Hyp	Ref	Expression
1		3bitri.1	. 2 |- (ph <-> ps)
2		3bitri.2	. . 3 |- (ps <-> ch)
3		3bitri.3	. . 3 |- (ch <-> th)
4	2, 3	bitri 190	. 2 |- (ps <-> th)
5	1, 4	bitri 190	1 |- (ph <-> th)

Syntax hints:   <-> wb 163

This theorem is referenced by:  orbi1i 276  orass 280  or23 284  pm4.14 379  pm4.15 380  anbi1i 539  bibi2iOLD 670  bibi1i 671  pm5.32 706  pm5.55 739  rnlemOLD 854  an6 1177  nic-axALT 1240  19.43 1440  alrot4 1451  excom13 1452  sb3an 1608  19.12vv 1681  19.12vvOLD 1682  3exdistr 1693  3exdistrOLD 1694  4exdistr 1695  eeeanv 1708  ee4anv 1710  elsb3 1718  elsb4 1720  2exsb 1742  sb8eu 1783  2eu4 1856  2eu6 1858  2eu7 1859  2eu8 1860  clelsb3 1990  r19.29OLD 2228  cbvreuv 2282  ceqsex2 2326  ceqsex2OLD 2327  ceqsex3v 2330  ceqsex4v 2331  ceqsex6v 2332  ceqsex8v 2333  gencbvexOLD 2335  euind 2439  reu2 2442  reu6 2443  rmo4 2445  reu8 2448  reuind 2450  sbralie 2453  elrabsf 2486  difjustOLD 2596  unjustOLD 2599  injustOLD 2602  dfss2 2610  ss2rab 2683  rabss 2684  ssrab 2685  rexun 2783  dfss4 2827  undif3 2854  symdif2OLD 2858  reuun2 2873  dfnul2 2877  abn0 2892  disj 2914  disj4 2922  inssdif0OLD 2941  sbsslem 2978  sbsslemOLD 2979  elimif 3001  eltp 3074  ralprg 3078  ralprOLDOLD 3081  ralsn 3084  disjsn 3089  r19.12sn 3093  difprsnOLD 3128  prsspwOLD 3151  preqsn 3157  uni0b 3203  uni0c 3204  unissb 3208  ssint 3232  ssintab 3233  ssintabOLD 3234  iunconstOLD 3263  dfiin2 3287  dfiin2OLD 3288  iunss 3291  iunssOLD 3292  iunrab 3299  ssiinOLD 3303  iunn0OLD 3316  iinxsng 3325  iinxprg 3326  iunxsn 3327  iunxun 3329  dftr5 3414  truni 3425  trint 3426  inuni 3470  axpweq 3480  ssextss 3507  exss 3516  eqvinop 3536  opeqsn 3549  opeqpr 3550  opelopabsb 3564  brabsb 3566  opabn0 3575  dfid3 3587  posn 3603  sotrieq 3616  wereu 3654  ordtri3orOLD 3692  ordtri1OLD 3694  ordtri3OLD 3698  uniuni 3806  euuni 3807  reusn 3818  reusnOLD 3819  eufromeq4 3831  dfwe2OLD 3862  ordpwsuc 3896  onzslOLD 3929  dflim3 3930  dfom2 3951  elvvv 4054  ssrel 4075  reliun 4101  relop 4113  cnvcoOLD 4146  cnvuni 4147  dmuni 4166  dmopab3 4169  dmcosseqOLD 4215  opelres 4222  dfima2OLD 4266  elimasnOLD 4290  asymref 4308  asymrefOLD 4309  asymref2 4310  asymref2OLD 4311  intirr 4312  intirrOLD 4313  rnuni 4327  xpeq0 4336  ssrnres 4354  dminxp 4357  dmsnn0 4362  cnvsn 4373  elxp4 4379  elxp5 4380  dfco2aOLD 4395  imaco 4403  rnco 4404  coi1 4413  cnvpo 4427  dffun2 4431  fncnv 4479  fun11 4480  isarep1 4497  isarep1OLD 4498  fcoi1OLD 4585  fcoi2OLD 4587  f1cnv 4611  dff1o2 4639  dff1o4 4644  dff1o5OLD 4647  fv2OLD 4677  eqfnfv3 4769  fnressn 4812  imaiun 4840  dff13 4850  dff1o6 4853  foprab2 5061  elrnoprabg 5066  fparlem1 5081  fparlem2 5082  fparlem3 5083  fparlem4 5084  dfrdg2 5141  tz7.48lem 5164  tz7.49c 5169  oaord 5228  eqerlem 5328  uniqs 5354  th3qlem1 5373  mapsnen 5488  xpsnen 5494  xpassen 5500  pw2en 5505  dom0 5528  abfii2 5652  ordiso 5683  tz9.12lem3 5772  ranksn 5800  rankeq0 5807  rankxpsuc 5826  cp 5852  aceq5lem1 5897  aceq5lem2 5898  aceq5lem5 5901  kmlem3 5929  kmlem12 5938  kmlem13 5939  kmlem14 5940  kmlem15 5941  aceqkm 5943  cf0 6058  ltpiord 6167  genpn0 6258  genpass 6264  distrlem1pr 6279  psslinpr 6287  suplem1pr 6313  suplem2pr 6314  mappsrpr 6370  opelreal 6401  elreal 6402  neg11i 6566  ltxr 6664  elxr 6706  ssxrOLD 6715  lesubaddiOLD 6772  halfposi 7087  xrsupss 7287  xrinfmss 7288  elnn0 7310  elnn0z 7356  elznn0nn 7357  raluz2 7612  rexuz2 7614  nnwos 7629  elfzuzb 7646  fzprval 7687  fztpval 7688  sqeqori 7893  cjrebi 8031  negrebi 8045  abs00i 8093  cau3iri 8167  cau5i 8171  bcpasci 8221  expcnvlem2 8489  infpn2 8778  ruclem1 8779  ruclem3 8781  infxpidmlem8 8828  infxpidmlem9 8829  istps3 8877  tgval2 8887  subbas 8914  subtop 8916  cctop 8922  qdensere 9027  spwpr2 10001  pilem1 10020  grothpw 10134  filrn 10293  hlimcauii 10739  choc0 10923  shlesb1i 10992  shne0i 11004  chnlei 11041  h1deoi 11105  cmbr2i 11172  pjss2i 11260  pjneli 11303  ho02i 11392  adjsym 11396  lnopeqi 11570  dfpjop 11755  largei 11839  atoml2i 11955  cdj3lem3b 12012  bnj170OLD 12035  bnj173OLD 12041  bnj174OLD 12043  bnj176OLD 12046  bnj179OLD 12050  bnj345 12187  bnj11OLD 12377  bnj13 12378  bnj14OLD 12382  bnj29 12394  bnj33OLD 12402  bnj47OLD 12418  bnj48OLD 12423  bnj51 12426  bnj55 12430  bnj58 12431  bnj77OLD 12438  bnj79OLD 12441  bnj80 12442  bnj89 12444  bnj88 12447  bnj112 12457  bnj115 12459  bnj142 12474  bnj156 12482  bnj158 12483  bnj220 12511  bnj537 12533  bnj538 12534  bnj921 12828  bnj919 12829  bnj979 12863  bnj1046 12887  bnj1164 12956  bnj1215 12991  bnj1222 12995  bnj1366 13091  bnj1392 13106  bnj1393 13107  bnj82 13210  bnj86 13213  bnj87 13214  bnj92 13216  bnj124 13234  bnj125 13235  bnj126 13236  bnj149 13241  bnj154 13245  bnj155 13246  bnj207 13248  bnj523 13262  bnj526 13263  bnj539 13266  bnj540 13267  bnj541 13268  bnj571 13289  bnj581 13294  bnj611 13307  bnj916 13332  bnj965 13346  bnj983 13357  bnj1000 13364  bnj1037 13386  bnj1039 13387  bnj1041 13389  bnj1042 13390  bnj1043 13391  bnj1045 13392  bnj1069 13400  bnj1081 13407  bnj1123 13422  bnj1134 13427  bnj1128 13428  bnj1398 13515  divalglem10 13705  gcdcllem1 13718  truniOLD 13792  trintOLD 13794  3orit 13811  elres 13824  elsnres 13825  brtp 13830  dffr5 13831  dftr6 13834  dfon2lem5 13853  19.12b 13868  sspred 13886  predreseq 13890  wfi 13915  eltrcl 13932  trclss 13935  frind 13939  xporderlem 13948  frxp 13951  axfelem15 14045  axfelem16 14046  brtxp 14067  brsset 14069  dfon3 14072  brbigcup 14074  elfix 14077  ellimits 14079  TFSid 14125  FTSid 14126  df3nandALT2 14147  tbw-bijust 14165  rb-bijust 14216  anddi2 14268  eeeeanv 14272  excxor 14280  r19.26t 14282  albineal 14323  ref4w 14370  dff1o6f 14416  definc 14621  dfdir2 14639  isdir2 14640  hmeogrp 14892  sbtpsines 14905  cnvresima 15359  ordisoOLD 15374  subntr 15425  compsub 15431  compfipin0 15436  alexsublem3 15439  alexsublem4 15440  reconnlem1 15446  cnfillim 15590  rexunOLD 15656  difin2 15676  difxp 15690  opabex3 15701  eqfnfv3OLD 15721  pofun 15772  fimaxre 15774  isbnd3 15941  heiborlem24 15978  heiborlem29 15983  prtlem70 16238  prtlem5 16245  0nelqs2 16269  prter2 16285  pm13.196a 16378  elnev 16404  compne 16417  strdif 16719  isposNEW 16773  isopos 16909  isgrpNEW 17104  isringNEW 17142  issrng 17176  islvec 17188  isphil 17195  ispsubsp2 17227  pmapglb 17252  polval2 17319

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

Copyright terms: Public domain