Theorem bitr2id 283

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitr3di  285  necon1abid  2969  necon4abid  2971  uniiunlem  4081  r19.9rzv  4500  2reu4lem  4526  intprg  4984  inimasn  6160  fnresdisj  6674  fnsnfv  6974  f1oiso  7356  reldm  8047  rdglim2  8451  mptelixpg  8952  1idpr  11052  nndiv  12288  fz1sbc  13609  grpid  18937  isrnghm  20385  rnghmval2  20388  znleval  21493  fbunfip  23804  lmflf  23940  metcld2  25266  lgsne0  27299  isuvtx  29265  loopclwwlkn1b  29909  clwwlknun  29979  frgrncvvdeqlem2  30167  isph  30689  ofpreima  32511  ressply1mon1p  33340  eulerpartlemd  34073  bnj168  34448  cardpred  34800  opelco3  35457  wl-2sb6d  37112  poimirlem26  37206  cnambfre  37228  heibor1  37370  opltn0  38748  cvrnbtwn2  38833  cvrnbtwn4  38837  atlltn0  38864  pmapjat1  39412  dih1dimatlem  40888  2rexfrabdioph  42298  dnwech  42554  rfovcnvf1od  43516  uneqsn  43537  lighneallem2  47025