Theorem bitr4i 187

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

Hypotheses

Ref	Expression
bitr4i.1	⊢ (𝜑 ↔ 𝜓)
bitr4i.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
bitr4i	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitr4i

Step	Hyp	Ref	Expression
1		bitr4i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		bitr4i.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	bicomi 132	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 184	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr2i  208  3bitr2ri  209  3bitr4i  212  3bitr4ri  213  biancomi  270  imdistan  444  bianass  469  biadani  616  mpbiran  948  mpbiran2  949  3anrev  1014  an6  1357  nfand  1616  19.33b2  1677  nf3  1717  nf4dc  1718  nf4r  1719  equsalh  1774  sb6x  1827  sb5f  1852  sbidm  1899  sb5  1936  sbanv  1938  sborv  1939  sbhb  1993  sb3an  2011  sbel2x  2051  sbal1yz  2054  sbexyz  2056  eu2  2124  2eu4  2173  cleqh  2331  cleqf  2399  dcne  2413  necon3bii  2440  ne3anior  2490  r2alf  2549  r2exf  2550  r19.23t  2640  r19.26-3  2663  r19.26m  2664  r19.43  2691  rabid2  2710  isset  2809  ralv  2820  rexv  2821  reuv  2822  rmov  2823  rexcom4b  2828  ceqsex4v  2847  ceqsex8v  2849  ceqsrexv  2936  ralrab2  2971  rexrab2  2973  reu2  2994  reu3  2996  reueq  3005  2reuswapdc  3010  reuind  3011  sbc3an  3093  rmo2ilem  3122  csbcow  3138  ssalel  3215  dfss3  3216  dfss3f  3219  ssabral  3298  rabss  3304  ssrabeq  3314  uniiunlem  3316  dfdif3  3317  ddifstab  3339  uncom  3351  inass  3417  indi  3454  difindiss  3461  difin2  3469  reupick3  3492  n0rf  3507  eq0  3513  eqv  3514  vss  3542  disj  3543  disj3  3547  undisj1  3552  undisj2  3553  exsnrex  3711  euabsn2  3740  euabsn  3741  snmb  3793  prssg  3830  dfuni2  3895  unissb  3923  elint2  3935  ssint  3944  dfiin2g  4003  iunn0m  4031  iunxun  4050  iunxiun  4052  iinpw  4061  disjnim  4078  dftr2  4189  dftr5  4190  dftr3  4191  dftr4  4192  vnex  4220  inuni  4245  snelpw  4304  sspwb  4308  opelopabsb  4354  eusv2  4554  orddif  4645  onintexmid  4671  zfregfr  4672  tfi  4680  opthprc  4777  elxp3  4780  xpiundir  4785  elvv  4788  brinxp2  4793  relsn  4831  reliun  4848  inxp  4864  raliunxp  4871  rexiunxp  4872  cnvuni  4916  dm0rn0  4948  elrn  4975  ssdmres  5035  dfres2  5065  dfima2  5078  args  5105  cotr  5118  intasym  5121  asymref  5122  intirr  5123  cnv0  5140  xp11m  5175  cnvresima  5226  resco  5241  rnco  5243  coiun  5246  coass  5255  dfiota2  5287  dffun2  5336  dffun6f  5339  dffun4f  5342  dffun7  5353  dffun9  5355  funfn  5356  svrelfun  5395  imadiflem  5409  dffn2  5484  dffn3  5493  fintm  5522  dffn4  5565  dff1o4  5591  brprcneu  5632  eqfnfv3  5746  fnreseql  5757  fsn  5819  abrexco  5900  imaiun  5901  mpo2eqb  6131  elovmpo  6221  abexex  6288  releldm2  6348  fnmpo  6367  dftpos4  6429  tfrlem7  6483  0er  6736  eroveu  6795  erovlem  6796  map0e  6855  elixpconst  6875  domen  6922  reuen1  6975  xpf1o  7030  ssfilem  7062  ssfilemd  7064  finexdc  7092  pw1dc0el  7103  ssfirab  7129  sbthlemi10  7165  djuexb  7243  sspw1or2  7403  iftrueb01  7441  pw1if  7443  dmaddpq  7599  dmmulpq  7600  distrnqg  7607  enq0enq  7651  enq0tr  7654  nqnq0pi  7658  distrnq0  7679  prltlu  7707  prarloc  7723  genpdflem  7727  ltexprlemm  7820  ltexprlemlol  7822  ltexprlemupu  7824  ltexprlemdisj  7826  recexprlemdisj  7850  ltresr  8059  elnnz  9489  dfz2  9552  2rexuz  9816  eluz2b1  9835  elxr  10011  elixx1  10132  elioo2  10156  elioopnf  10202  elicopnf  10204  elfz1  10248  fzdifsuc  10316  fznn  10324  fzp1nel  10339  fznn0  10348  dfrp2  10524  redivap  11436  imdivap  11443  rexanre  11782  climreu  11859  prodmodc  12141  3dvdsdec  12428  3dvds2dec  12429  bitsval  12506  bezoutlembi  12578  nnwosdc  12612  isprm2  12691  isprm3  12692  isprm4  12693  pythagtriplem2  12841  elgz  12946  inffinp1  13052  isnsg4  13801  isrng  13950  isring  14016  dfrhm2  14171  lss1d  14400  isbasis3g  14773  restsn  14907  lmbr  14940  txbas  14985  tx2cn  14997  elcncf1di  15306  dedekindicclemicc  15359  limcrcl  15385  isclwwlk  16248  clwwlkccatlem  16254  eupth2lem1  16312  bj-nnor  16351  bj-vprc  16512  ss1oel2o  16607  subctctexmid  16622  trirec0xor  16670