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  4084  r19.9rzv  4499  2reu4lem  4525  intprg  4985  inimasn  6155  fnresdisj  6670  fnsnfv  6970  f1oiso  7350  reldm  8032  rdglim2  8434  mptelixpg  8931  1idpr  11026  nndiv  12262  fz1sbc  13581  grpid  18896  isrnghm  20332  rnghmval2  20335  znleval  21329  fbunfip  23593  lmflf  23729  metcld2  25048  lgsne0  27062  isuvtx  28907  loopclwwlkn1b  29550  clwwlknun  29620  frgrncvvdeqlem2  29808  isph  30330  ofpreima  32145  ressply1mon1p  32919  eulerpartlemd  33651  bnj168  34027  cardpred  34379  opelco3  35038  wl-2sb6d  36726  poimirlem26  36817  cnambfre  36839  heibor1  36981  opltn0  38363  cvrnbtwn2  38448  cvrnbtwn4  38452  atlltn0  38479  pmapjat1  39027  dih1dimatlem  40503  2rexfrabdioph  41836  dnwech  42092  rfovcnvf1od  43057  uneqsn  43078  lighneallem2  46573