Theorem bitr3i 184

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

Hypotheses

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

Assertion

Ref	Expression
bitr3i	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitr3i

Step	Hyp	Ref	Expression
1		bitr3i.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 130	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3i.2	. 2 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	bitri 182	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitrri  205  3bitr3i  208  3bitr3ri  209  anandi  554  anandir  555  xchnxbi  637  orordi  722  orordir  723  sbco3v  1884  elsb3  1893  elsb4  1894  sbco4  1924  abeq1i  2190  r19.41  2509  rexcom4a  2623  moeq  2767  mosubt  2769  2reuswapdc  2794  nfcdeq  2812  sbcid  2830  sbcco2  2837  sbc7  2841  sbcie2g  2847  eqsbc3  2853  sbcralt  2890  sbcrext  2891  cbvralcsf  2964  cbvrexcsf  2965  cbvrabcsf  2967  abss  3063  ssab  3064  difrab  3238  prsspw  3557  brab1  3830  unopab  3857  exss  3982  uniuni  4201  elvvv  4421  eliunxp  4493  ralxp  4497  rexxp  4498  opelco  4525  reldm0  4571  resieq  4640  resiexg  4673  iss  4674  imai  4701  cnvsym  4728  intasym  4729  asymref  4730  codir  4733  poirr2  4737  rninxp  4784  cnvsom  4881  funopg  4954  fin  5096  f1cnvcnv  5120  fndmin  5295  resoprab  5617  mpt22eqb  5630  ov6g  5658  offval  5739  dfopab2  5835  dfoprab3s  5836  fmpt2x  5846  spc2ed  5874  brtpos0  5890  dftpos3  5900  tpostpos  5902  ercnv  6150  xpcomco  6323  xpassen  6327  phpm  6351  elni2  6504  elfz2nn0  9128  elfzmlbp  9143  expival  9478  clim0  10124