Theorem bitr2id 286

Description: A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.)

Hypotheses

Ref	Expression
bitr2id.1	⊢ (𝜑 ↔ 𝜓)
bitr2id.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
bitr2id	⊢ (𝜒 → (𝜃 ↔ 𝜑))

Proof of Theorem bitr2id

Step	Hyp	Ref	Expression
1		bitr2id.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		bitr2id.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	bitrid 285	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 225	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  bitr3di  288  necon1abid  2985  necon4abid  2987  uniiunlem  4031  r19.9rzv  4449  2reu4lem  4467  intprg  4929  inimasn  6127  fnresdisj  6626  fnsnfv  6931  f1oiso  7320  reldm  8010  rdglim2  8387  mptelixpg  8902  1idpr  10973  nndiv  12245  fz1sbc  13591  grpid  18989  isrnghm  20458  rnghmval2  20461  znleval  21575  fbunfip  23898  lmflf  24034  metcld2  25338  lgsne0  27365  sltssnb  27828  isuvtx  29531  loopclwwlkn1b  30179  clwwlknun  30249  frgrncvvdeqlem2  30437  isph  30960  ofpreima  32806  fdifsupp  32826  ressply1mon1p  33708  eulerpartlemd  34607  bnj168  34973  cardpred  35333  opelco3  36063  qdiffALT  37758  wl-2sb6d  37999  poimirlem26  38083  cnambfre  38105  heibor1  38247  opltn0  39752  cvrnbtwn2  39837  cvrnbtwn4  39841  atlltn0  39868  pmapjat1  40415  dih1dimatlem  41891  2rexfrabdioph  43311  dnwech  43563  rfovcnvf1od  44518  uneqsn  44539  lighneallem2  48153  stgredgiun  48518  isinito2lem  50057