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  614  mpbiran  946  mpbiran2  947  3anrev  1012  an6  1355  nfand  1614  19.33b2  1675  nf3  1715  nf4dc  1716  nf4r  1717  equsalh  1772  sb6x  1825  sb5f  1850  sbidm  1897  sb5  1934  sbanv  1936  sborv  1937  sbhb  1991  sb3an  2009  sbel2x  2049  sbal1yz  2052  sbexyz  2054  eu2  2122  2eu4  2171  cleqh  2329  cleqf  2397  dcne  2411  necon3bii  2438  ne3anior  2488  r2alf  2547  r2exf  2548  r19.23t  2638  r19.26-3  2661  r19.26m  2662  r19.43  2689  rabid2  2708  isset  2806  ralv  2817  rexv  2818  reuv  2819  rmov  2820  rexcom4b  2825  ceqsex4v  2844  ceqsex8v  2846  ceqsrexv  2933  ralrab2  2968  rexrab2  2970  reu2  2991  reu3  2993  reueq  3002  2reuswapdc  3007  reuind  3008  sbc3an  3090  rmo2ilem  3119  csbcow  3135  ssalel  3212  dfss3  3213  dfss3f  3216  ssabral  3295  rabss  3301  ssrabeq  3311  uniiunlem  3313  dfdif3  3314  ddifstab  3336  uncom  3348  inass  3414  indi  3451  difindiss  3458  difin2  3466  reupick3  3489  n0rf  3504  eq0  3510  eqv  3511  vss  3539  disj  3540  disj3  3544  undisj1  3549  undisj2  3550  exsnrex  3708  euabsn2  3735  euabsn  3736  snmb  3788  prssg  3825  dfuni2  3890  unissb  3918  elint2  3930  ssint  3939  dfiin2g  3998  iunn0m  4026  iunxun  4045  iunxiun  4047  iinpw  4056  disjnim  4073  dftr2  4184  dftr5  4185  dftr3  4186  dftr4  4187  vnex  4215  inuni  4240  snelpw  4299  sspwb  4303  opelopabsb  4349  eusv2  4549  orddif  4640  onintexmid  4666  zfregfr  4667  tfi  4675  opthprc  4772  elxp3  4775  xpiundir  4780  elvv  4783  brinxp2  4788  relsn  4826  reliun  4843  inxp  4859  raliunxp  4866  rexiunxp  4867  cnvuni  4911  dm0rn0  4943  elrn  4970  ssdmres  5030  dfres2  5060  dfima2  5073  args  5100  cotr  5113  intasym  5116  asymref  5117  intirr  5118  cnv0  5135  xp11m  5170  cnvresima  5221  resco  5236  rnco  5238  coiun  5241  coass  5250  dfiota2  5282  dffun2  5331  dffun6f  5334  dffun4f  5337  dffun7  5348  dffun9  5350  funfn  5351  svrelfun  5389  imadiflem  5403  dffn2  5478  dffn3  5487  fintm  5516  dffn4  5559  dff1o4  5585  brprcneu  5625  eqfnfv3  5739  fnreseql  5750  fsn  5812  abrexco  5892  imaiun  5893  mpo2eqb  6123  elovmpo  6213  abexex  6280  releldm2  6340  fnmpo  6359  dftpos4  6420  tfrlem7  6474  0er  6727  eroveu  6786  erovlem  6787  map0e  6846  elixpconst  6866  domen  6913  reuen1  6966  xpf1o  7018  ssfilem  7050  finexdc  7078  pw1dc0el  7089  ssfirab  7114  sbthlemi10  7149  djuexb  7227  iftrueb01  7424  pw1if  7426  dmaddpq  7582  dmmulpq  7583  distrnqg  7590  enq0enq  7634  enq0tr  7637  nqnq0pi  7641  distrnq0  7662  prltlu  7690  prarloc  7706  genpdflem  7710  ltexprlemm  7803  ltexprlemlol  7805  ltexprlemupu  7807  ltexprlemdisj  7809  recexprlemdisj  7833  ltresr  8042  elnnz  9472  dfz2  9535  2rexuz  9794  eluz2b1  9813  elxr  9989  elixx1  10110  elioo2  10134  elioopnf  10180  elicopnf  10182  elfz1  10226  fzdifsuc  10294  fznn  10302  fzp1nel  10317  fznn0  10326  dfrp2  10500  redivap  11406  imdivap  11413  rexanre  11752  climreu  11829  prodmodc  12110  3dvdsdec  12397  3dvds2dec  12398  bitsval  12475  bezoutlembi  12547  nnwosdc  12581  isprm2  12660  isprm3  12661  isprm4  12662  pythagtriplem2  12810  elgz  12915  inffinp1  13021  isnsg4  13770  isrng  13918  isring  13984  dfrhm2  14139  lss1d  14368  isbasis3g  14741  restsn  14875  lmbr  14908  txbas  14953  tx2cn  14965  elcncf1di  15274  dedekindicclemicc  15327  limcrcl  15353  isclwwlk  16163  clwwlkccatlem  16169  bj-nnor  16207  bj-vprc  16368  ss1oel2o  16464  subctctexmid  16479  trirec0xor  16527