Theorem bitr3i 186

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 132	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3i.2	. 2 ⊢ (𝜓 ↔ 𝜒)
4	2, 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:  3bitrri  207  3bitr3i  210  3bitr3ri  211  anandi  590  anandir  591  xchnxbi  682  orordi  775  orordir  776  sbco3v  1998  sbco4  2036  elsb1  2184  elsb2  2185  abeq1i  2318  cbvabw  2329  r19.41  2662  rexcom4a  2797  moeq  2949  mosubt  2951  2reuswapdc  2978  nfcdeq  2996  sbcid  3015  sbcco2  3022  sbc7  3026  sbcie2g  3033  eqsbc1  3039  sbcralt  3076  sbcrext  3077  cbvralcsf  3157  cbvrexcsf  3158  cbvrabcsf  3160  abss  3263  ssab  3264  difrab  3448  abn0m  3487  prsspw  3808  disjnim  4037  brab1  4095  unopab  4127  exss  4275  uniuni  4502  elvvv  4742  eliunxp  4821  ralxp  4825  rexxp  4826  opelco  4854  reldm0  4901  resieq  4974  resiexg  5009  iss  5010  imai  5043  cnvsym  5071  intasym  5072  asymref  5073  codir  5076  poirr2  5080  rninxp  5131  cnvsom  5231  funopg  5310  fin  5469  f1cnvcnv  5499  fndmin  5694  resoprab  6048  mpo2eqb  6062  ov6g  6091  offval  6173  dfopab2  6282  dfoprab3s  6283  fmpox  6293  spc2ed  6326  brtpos0  6345  dftpos3  6355  tpostpos  6357  ercnv  6648  xpcomco  6928  xpassen  6932  phpm  6969  ctssdccl  7220  elni2  7434  elfz2nn0  10241  elfzmlbp  10261  clim0  11640  nnwosdc  12404  isstructim  12890  xpscf  13223  srgrmhm  13800  ntreq0  14648  cnmptcom  14814  dedekindicclemicc  15148