Theorem bitr3i 251

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 2-Jun-1993.)

Hypotheses

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

Assertion

Ref	Expression
bitr3i	|- ( ph <-> ch )

Proof of Theorem bitr3i

Step	Hyp	Ref	Expression
1		bitr3i.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 202	. 2 |- ( ph <-> ps )
3		bitr3i.2	. 2 |- ( ps <-> ch )
4	2, 3	bitri 249	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 184

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 185

This theorem is referenced by:  3bitrri  272  3bitr3i  275  3bitr3ri  276  xchnxbi  306  ianor  486  orordi  528  orordir  529  anandi  829  anandir  830  trunantru  1449  falnanfal  1453  had0  1491  had0OLD  1492  nic-axALT  1527  sbied  2175  sbidm  2180  sb6a  2216  sbelx  2226  sbco4  2234  mo  2280  2eu6  2334  2eu6OLD  2335  bm1.1  2385  abeq1iOLD  2532  cbvab  2543  necon1bbiiOLD  2668  nabbi  2736  r19.41v  2958  r19.41  2959  2ralor  2976  rexcom4a  3079  moeq  3224  2reuswap  3251  2reu5  3257  nfcdeq  3273  sbcid  3293  sbcco2  3300  sbc7  3304  sbcie2g  3310  eqsbc3  3316  sbcralt  3349  cbvralcsf  3404  cbvrabcsf  3407  abss  3507  ssab  3508  difrab  3723  euelss  3736  neq0  3748  sbccsb  3797  vdif0  3829  difrab0eq  3830  ssunsn2  4130  sspr  4134  sstp  4135  prsspwOLD  4144  uniintsn  4264  rabasiun  4274  brab1  4439  unopab  4469  axrep5  4511  axsep  4515  intexab  4551  reusv2lem4  4597  reusv2  4599  reuxfrd  4615  wefrc  4816  elvvv  4882  eliunxp  4960  ralxp  4964  rexxp  4965  opelco  4994  reldm0  5040  resieq  5103  iss  5140  imai  5168  cnvsym  5201  intasym  5202  asymref  5203  codir  5207  poirr2  5211  xpdifid  5252  rninxp  5263  tz6.26  5397  wfis2fg  5403  ordelord  5431  dffun3  5579  funopg  5600  fin  5747  f1cnvcnv  5771  funimass4  5899  fnressn  6062  resoprab  6378  mpt22eqb  6391  elrnmpt2res  6396  ov6g  6420  offval  6527  uniuni  6590  dfwe2  6598  orduniorsuc  6647  tfinds2  6680  resiexg  6719  dfopab2  6837  dfoprab3s  6838  fmpt2x  6849  fparlem1  6883  fparlem2  6884  brtpos0  6964  dftpos3  6975  tpostpos  6977  dfrecs3  7075  tz7.48lem  7142  omeu  7270  ercnv  7368  ixp0  7539  xpcomco  7644  xpassen  7648  php  7738  findcard3  7796  ixpfi2  7851  dfsup2  7935  card2on  8013  infeq5i  8085  cnfcom3lem  8178  cnfcom3lemOLD  8186  r1elss  8255  rankxplim  8328  scott0s  8337  aceq1  8529  dfac5lem1  8535  dfac5lem2  8536  kmlem3  8563  kmlem8  8568  kmlem16  8576  cflem  8657  cf0  8662  alephval2  8978  rankcf  9184  r1tskina  9189  wfgru  9223  genpass  9416  psslinpr  9438  ltpsrpr  9515  infm3  10541  nnwos  11193  ioo0  11606  ico0  11627  ioc0  11628  icc0  11629  elfz2nn0  11822  elfzmlbp  11839  sqeqori  12322  hashgt12el  12528  hashgt12el2  12529  cshwidxmod  12828  clim0  13476  divalglem6  14263  isprm2lem  14431  pceu  14577  prmreclem2  14642  cshwshash  14796  isstruct  14849  xpscf  15178  acsfn2  15275  invsym2  15374  pospo  15925  f1omvdco3  16796  psgnunilem5  16841  efgrelexlemb  17090  gexex  17181  srgrmhm  17505  lssne0  17915  opsrtoslem1  18466  opsrtoslem2  18467  islindf4  19163  mdetunilem8  19411  cpmatmcllem  19509  pmatcollpw2lem  19568  ntreq0  19869  ordtrest2lem  19995  ist0-3  20137  ist1-2  20139  ist1-3  20141  cmpfi  20199  2ndcctbss  20246  ptbasfi  20372  ptcnplem  20412  hausdiag  20436  hauseqlcld  20437  cnmptcom  20469  txflf  20797  tgphaus  20905  metrest  21317  iccpnfcnv  21734  bcth3  22060  volun  22245  dyadmax  22297  vitalilem2  22308  vitalilem3  22309  mbfimaopnlem  22352  itg2leub  22431  dvres2  22606  ellogdm  23312  reasinsin  23550  leibpilem2  23595  ftalem3  23727  dchreq  23912  legso  24367  axcontlem2  24672  rusgranumwlklem0  25352  frgra3v  25406  4cycl2vnunb  25421  vdn0frgrav2  25427  vdgn0frgrav2  25428  usg2spot2nb  25469  lnon0  26113  spansncvi  26970  pjssmii  26999  nmlnopgt0i  27315  largei  27585  cvexchlem  27686  xfree  27762  spc2ed  27771  nmo  27785  2reuswap2  27788  fpwrelmapffslem  27988  addeq0  27991  eliccioo  28065  qtophaus  28278  ordtrest2NEWlem  28343  ordtconlem1  28345  xrge0iifcnv  28354  xrge0iifiso  28356  xrge0iifhom  28358  cntnevol  28662  eulerpartlemgh  28809  ballotlemfp1  28922  ballotlem7  28966  signswch  29010  bnj446  29083  bnj563  29114  bnj110  29230  bnj153  29252  bnj864  29294  bnj865  29295  bnj849  29297  bnj929  29308  bnj1110  29352  derang0  29453  iccllyscon  29534  cvmsss2  29558  elmrsubrn  29719  quad3  29863  axacprim  29895  dftr6  29950  dfpo2  29955  opelco3  29980  elima4  29981  setinds2f  29985  elpotr  29987  frins2fg  30045  wzel  30067  nobndlem1  30139  elfuns  30240  dfiota3  30248  imagesset  30278  lineunray  30472  ellines  30477  hfninf  30511  bj-axrep5  30929  bj-axsep  30930  bj-rexcom4a  30997  bj-snglc  31079  finixpnum  31390  fin2so  31392  tan2h  31399  ovoliunnfl  31408  voliunnfl  31410  ftc1anc  31451  inixp  31481  heibor1lem  31567  csbcom2fi  31796  tsna1  31813  islshpat  32015  lkr0f  32092  lshpsmreu  32107  cvrnbtwn4  32277  ishlat2  32351  islvol5  32576  tendoeq2  33773  dibelval3  34147  mapdpglem3  34675  hdmapglem7a  34930  4rexfrabdioph  35073  dford4  35313  isdomn3  35508  fgraphopab  35514  ifpim123g  35571  ifpbibib  35581  iunrelexpuztr  35678  dffrege115  35939  undisjrab  36014  radcnvrat  36023  opelopab4  36328  2sb5nd  36337  un2122  36591  uunT12p4  36604  onfrALTlem5VD  36696  2sb5ndVD  36721  2sb5ndALT  36743  ellimcabssub0  36972  fourierdlem42  37280  2rmoswap  37538  ndmaovcom  37639  nnsum4primesodd  37825  nnsum4primesoddALTV  37826  usgra2pth0  37965  eliunxp2  38415  pgrpgt2nabl  38451  islindeps  38546  lindslinindsimp1  38550  lindslinindsimp2  38556