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  2979  necon4abid  2981  uniiunlem  4083  r19.9rzv  4498  2reu4lem  4524  intprg  4984  inimasn  6152  fnresdisj  6667  fnsnfv  6967  f1oiso  7344  reldm  8026  rdglim2  8428  mptelixpg  8925  1idpr  11020  nndiv  12254  fz1sbc  13573  grpid  18856  znleval  21101  fbunfip  23364  lmflf  23500  metcld2  24815  lgsne0  26827  isuvtx  28641  loopclwwlkn1b  29284  clwwlknun  29354  frgrncvvdeqlem2  29542  isph  30062  ofpreima  31877  ressply1mon1p  32645  eulerpartlemd  33353  bnj168  33729  cardpred  34081  opelco3  34734  wl-2sb6d  36411  poimirlem26  36502  cnambfre  36524  heibor1  36666  opltn0  38048  cvrnbtwn2  38133  cvrnbtwn4  38137  atlltn0  38164  pmapjat1  38712  dih1dimatlem  40188  2rexfrabdioph  41519  dnwech  41775  rfovcnvf1od  42740  uneqsn  42761  lighneallem2  46260  isrnghm  46675  rnghmval2  46678