Theorem bitr3i 185

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 131	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3i.2	. 2 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	bitri 183	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrri  206  3bitr3i  209  3bitr3ri  210  anandi  579  anandir  580  xchnxbi  669  orordi  762  orordir  763  sbco3v  1942  elsb3  1951  elsb4  1952  sbco4  1982  abeq1i  2251  cbvabw  2262  r19.41  2586  rexcom4a  2710  moeq  2859  mosubt  2861  2reuswapdc  2888  nfcdeq  2906  sbcid  2924  sbcco2  2931  sbc7  2935  sbcie2g  2942  eqsbc3  2948  sbcralt  2985  sbcrext  2986  cbvralcsf  3062  cbvrexcsf  3063  cbvrabcsf  3065  abss  3166  ssab  3167  difrab  3350  abn0m  3388  prsspw  3692  disjnim  3920  brab1  3975  unopab  4007  exss  4149  uniuni  4372  elvvv  4602  eliunxp  4678  ralxp  4682  rexxp  4683  opelco  4711  reldm0  4757  resieq  4829  resiexg  4864  iss  4865  imai  4895  cnvsym  4922  intasym  4923  asymref  4924  codir  4927  poirr2  4931  rninxp  4982  cnvsom  5082  funopg  5157  fin  5309  f1cnvcnv  5339  fndmin  5527  resoprab  5867  mpo2eqb  5880  ov6g  5908  offval  5989  dfopab2  6087  dfoprab3s  6088  fmpox  6098  spc2ed  6130  brtpos0  6149  dftpos3  6159  tpostpos  6161  ercnv  6450  xpcomco  6720  xpassen  6724  phpm  6759  ctssdccl  6996  elni2  7129  elfz2nn0  9899  elfzmlbp  9916  clim0  11061  isstructim  11983  ntreq0  12311  cnmptcom  12477  dedekindicclemicc  12789