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  598  anandir  599  xchnxbi  691  orordi  785  orordir  786  sbco3v  2029  sbco4  2067  elsb1  2216  elsb2  2217  abeq1i  2350  cbvabw  2363  r19.41  2706  rexcom4a  2846  moeq  3001  mosubt  3003  2reuswapdc  3030  nfcdeq  3048  sbcid  3067  sbcco2  3074  sbc7  3078  sbcie2g  3085  eqsbc1  3091  sbcralt  3128  sbcrext  3129  cbvralcsf  3210  cbvrexcsf  3211  cbvrabcsf  3213  abss  3317  ssab  3318  difrab  3507  abn0m  3547  prsspw  3888  disjnim  4118  brab1  4176  unopab  4208  exss  4365  uniuni  4595  elvvv  4836  eliunxp  4917  ralxp  4921  rexxp  4922  opelco  4950  reldm0  4997  resieq  5071  resiexg  5106  iss  5107  imai  5141  cnvsym  5169  intasym  5170  asymref  5171  codir  5174  poirr2  5178  rninxp  5229  cnvsom  5329  funopg  5409  fin  5576  f1cnvcnv  5607  fndmin  5810  resoprab  6178  mpo2eqb  6192  ov6g  6221  offval  6304  dfopab2  6417  dfoprab3s  6418  fmpox  6430  spc2ed  6463  brtpos0  6517  dftpos3  6527  tpostpos  6529  ercnv  6822  xpcomco  7118  xpassen  7122  phpm  7161  ctssdccl  7445  elni2  7675  addeq0  8697  elfz2nn0  10502  elfzmlbp  10522  clim0  12034  nnwosdc  12799  ballotfilem7  13262  isstructim  13349  xpscf  13651  srgrmhm  14281  ntreq0  15216  cnmptcom  15382  dedekindicclemicc  15716