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  592  anandir  593  xchnxbi  684  orordi  778  orordir  779  sbco3v  2020  sbco4  2058  elsb1  2207  elsb2  2208  abeq1i  2341  cbvabw  2352  r19.41  2686  rexcom4a  2824  moeq  2978  mosubt  2980  2reuswapdc  3007  nfcdeq  3025  sbcid  3044  sbcco2  3051  sbc7  3055  sbcie2g  3062  eqsbc1  3068  sbcralt  3105  sbcrext  3106  cbvralcsf  3187  cbvrexcsf  3188  cbvrabcsf  3190  abss  3293  ssab  3294  difrab  3478  abn0m  3517  prsspw  3843  disjnim  4073  brab1  4131  unopab  4163  exss  4314  uniuni  4543  elvvv  4784  eliunxp  4864  ralxp  4868  rexxp  4869  opelco  4897  reldm0  4944  resieq  5018  resiexg  5053  iss  5054  imai  5087  cnvsym  5115  intasym  5116  asymref  5117  codir  5120  poirr2  5124  rninxp  5175  cnvsom  5275  funopg  5355  fin  5517  f1cnvcnv  5547  fndmin  5747  resoprab  6109  mpo2eqb  6123  ov6g  6152  offval  6235  dfopab2  6344  dfoprab3s  6345  fmpox  6357  spc2ed  6390  brtpos0  6409  dftpos3  6419  tpostpos  6421  ercnv  6714  xpcomco  6998  xpassen  7002  phpm  7040  ctssdccl  7294  elni2  7517  elfz2nn0  10325  elfzmlbp  10345  clim0  11817  nnwosdc  12581  isstructim  13067  xpscf  13401  srgrmhm  13978  ntreq0  14827  cnmptcom  14993  dedekindicclemicc  15327