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  1716  nf4dc  1717  nf4r  1718  equsalh  1773  sb6x  1826  sb5f  1851  sbidm  1898  sb5  1935  sbanv  1937  sborv  1938  sbhb  1992  sb3an  2010  sbel2x  2050  sbal1yz  2053  sbexyz  2055  eu2  2123  2eu4  2172  cleqh  2330  cleqf  2398  dcne  2412  necon3bii  2439  ne3anior  2489  r2alf  2548  r2exf  2549  r19.23t  2639  r19.26-3  2662  r19.26m  2663  r19.43  2690  rabid2  2709  isset  2808  ralv  2819  rexv  2820  reuv  2821  rmov  2822  rexcom4b  2827  ceqsex4v  2846  ceqsex8v  2848  ceqsrexv  2935  ralrab2  2970  rexrab2  2972  reu2  2993  reu3  2995  reueq  3004  2reuswapdc  3009  reuind  3010  sbc3an  3092  rmo2ilem  3121  csbcow  3137  ssalel  3214  dfss3  3215  dfss3f  3218  ssabral  3297  rabss  3303  ssrabeq  3313  uniiunlem  3315  dfdif3  3316  ddifstab  3338  uncom  3350  inass  3416  indi  3453  difindiss  3460  difin2  3468  reupick3  3491  n0rf  3506  eq0  3512  eqv  3513  vss  3541  disj  3542  disj3  3546  undisj1  3551  undisj2  3552  exsnrex  3712  euabsn2  3741  euabsn  3742  snmb  3794  prssg  3831  dfuni2  3896  unissb  3924  elint2  3936  ssint  3945  dfiin2g  4004  iunn0m  4032  iunxun  4051  iunxiun  4053  iinpw  4062  disjnim  4079  dftr2  4190  dftr5  4191  dftr3  4192  dftr4  4193  vnex  4221  inuni  4246  snelpw  4306  sspwb  4310  opelopabsb  4356  eusv2  4556  orddif  4647  onintexmid  4673  zfregfr  4674  tfi  4682  opthprc  4779  elxp3  4782  xpiundir  4787  elvv  4790  brinxp2  4795  relsn  4833  reliun  4850  inxp  4866  raliunxp  4873  rexiunxp  4874  cnvuni  4918  dm0rn0  4950  elrn  4977  ssdmres  5037  dfres2  5067  dfima2  5080  args  5107  cotr  5120  intasym  5123  asymref  5124  intirr  5125  cnv0  5142  xp11m  5177  cnvresima  5228  resco  5243  rnco  5245  coiun  5248  coass  5257  dfiota2  5289  dffun2  5338  dffun6f  5341  dffun4f  5344  dffun7  5355  dffun9  5357  funfn  5358  svrelfun  5397  imadiflem  5411  dffn2  5486  dffn3  5495  fintm  5524  dffn4  5568  dff1o4  5594  brprcneu  5635  eqfnfv3  5749  fnreseql  5760  fsn  5822  abrexco  5905  imaiun  5906  mpo2eqb  6136  elovmpo  6226  abexex  6293  releldm2  6353  fnmpo  6372  dftpos4  6434  tfrlem7  6488  0er  6741  eroveu  6800  erovlem  6801  map0e  6860  elixpconst  6880  domen  6927  reuen1  6980  xpf1o  7035  ssfilem  7067  ssfilemd  7069  finexdc  7097  pw1dc0el  7108  ssfirab  7134  sbthlemi10  7170  djuexb  7248  sspw1or2  7408  iftrueb01  7446  pw1if  7448  dmaddpq  7604  dmmulpq  7605  distrnqg  7612  enq0enq  7656  enq0tr  7659  nqnq0pi  7663  distrnq0  7684  prltlu  7712  prarloc  7728  genpdflem  7732  ltexprlemm  7825  ltexprlemlol  7827  ltexprlemupu  7829  ltexprlemdisj  7831  recexprlemdisj  7855  ltresr  8064  elnnz  9494  dfz2  9557  2rexuz  9821  eluz2b1  9840  elxr  10016  elixx1  10137  elioo2  10161  elioopnf  10207  elicopnf  10209  elfz1  10253  fzdifsuc  10321  fznn  10329  fzp1nel  10344  fznn0  10353  dfrp2  10529  redivap  11457  imdivap  11464  rexanre  11803  climreu  11880  prodmodc  12162  3dvdsdec  12449  3dvds2dec  12450  bitsval  12527  bezoutlembi  12599  nnwosdc  12633  isprm2  12712  isprm3  12713  isprm4  12714  pythagtriplem2  12862  elgz  12967  inffinp1  13073  isnsg4  13822  isrng  13971  isring  14037  dfrhm2  14192  lss1d  14421  isbasis3g  14799  restsn  14933  lmbr  14966  txbas  15011  tx2cn  15023  elcncf1di  15332  dedekindicclemicc  15385  limcrcl  15411  isclwwlk  16274  clwwlkccatlem  16280  eupth2lem1  16338  bj-nnor  16391  bj-vprc  16551  ss1oel2o  16646  subctctexmid  16661  trirec0xor  16716