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  2985  necon4abid  2987  uniiunlem  4110  r19.9rzv  4523  2reu4lem  4545  intprg  5005  inimasn  6187  fnresdisj  6700  fnsnfv  7001  f1oiso  7387  reldm  8085  rdglim2  8488  mptelixpg  8993  1idpr  11098  nndiv  12339  fz1sbc  13660  grpid  19015  isrnghm  20467  rnghmval2  20470  znleval  21596  fbunfip  23898  lmflf  24034  metcld2  25360  lgsne0  27397  isuvtx  29430  loopclwwlkn1b  30074  clwwlknun  30144  frgrncvvdeqlem2  30332  isph  30854  ofpreima  32683  ressply1mon1p  33558  eulerpartlemd  34331  bnj168  34706  cardpred  35066  opelco3  35738  wl-2sb6d  37512  poimirlem26  37606  cnambfre  37628  heibor1  37770  opltn0  39146  cvrnbtwn2  39231  cvrnbtwn4  39235  atlltn0  39262  pmapjat1  39810  dih1dimatlem  41286  2rexfrabdioph  42752  dnwech  43005  rfovcnvf1od  43966  uneqsn  43987  lighneallem2  47480