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  7299  reldm  7990  rdglim2  8365  mptelixpg  8877  1idpr  10944  nndiv  12195  fz1sbc  13520  grpid  18909  isrnghm  20381  rnghmval2  20384  znleval  21513  fbunfip  23817  lmflf  23953  metcld2  25267  lgsne0  27306  ssltsnb  27769  isuvtx  29451  loopclwwlkn1b  30100  clwwlknun  30170  frgrncvvdeqlem2  30358  isph  30880  ofpreima  32725  fdifsupp  32745  ressply1mon1p  33630  eulerpartlemd  34504  bnj168  34867  cardpred  35229  opelco3  35950  wl-2sb6d  37734  poimirlem26  37818  cnambfre  37840  heibor1  37982  opltn0  39487  cvrnbtwn2  39572  cvrnbtwn4  39576  atlltn0  39603  pmapjat1  40150  dih1dimatlem  41626  2rexfrabdioph  43074  dnwech  43326  rfovcnvf1od  44281  uneqsn  44302  lighneallem2  47888  stgredgiun  48240  isinito2lem  49779