Theorem bitr2id 284

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 283	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 223	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bitr3di  286  necon1abid  2971  necon4abid  2973  uniiunlem  4040  r19.9rzv  4459  2reu4lem  4477  intprg  4937  inimasn  6115  fnresdisj  6613  fnsnfv  6914  f1oiso  7300  reldm  7991  rdglim2  8366  mptelixpg  8878  1idpr  10945  nndiv  12196  fz1sbc  13521  grpid  18910  isrnghm  20382  rnghmval2  20385  znleval  21514  fbunfip  23818  lmflf  23954  metcld2  25268  lgsne0  27307  sltssnb  27770  isuvtx  29473  loopclwwlkn1b  30122  clwwlknun  30192  frgrncvvdeqlem2  30380  isph  30902  ofpreima  32747  fdifsupp  32767  ressply1mon1p  33653  eulerpartlemd  34536  bnj168  34899  cardpred  35261  opelco3  35982  wl-2sb6d  37776  poimirlem26  37860  cnambfre  37882  heibor1  38024  opltn0  39529  cvrnbtwn2  39614  cvrnbtwn4  39618  atlltn0  39645  pmapjat1  40192  dih1dimatlem  41668  2rexfrabdioph  43116  dnwech  43368  rfovcnvf1od  44323  uneqsn  44344  lighneallem2  47929  stgredgiun  48281  isinito2lem  49820