Theorem bitr2id 287

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitr3di  289  necon1abid  2994  necon4abid  2996  uniiunlem  4040  r19.9rzv  4465  2reu4lem  4483  intprg  4945  inimasn  6153  fnresdisj  6655  fnsnfv  6960  f1oiso  7349  reldm  8040  rdglim2  8418  mptelixpg  8932  1idpr  11013  nndiv  12281  fz1sbc  13627  grpid  19041  isrnghm  20522  rnghmval2  20525  znleval  21683  fbunfip  24005  lmflf  24141  metcld2  25445  lgsne0  27475  sltssnb  27938  isuvtx  29711  loopclwwlkn1b  30359  clwwlknun  30429  frgrncvvdeqlem2  30617  isph  31140  ofpreima  32976  fdifsupp  32996  ressply1mon1p  33824  eulerpartlemd  34722  bnj168  35085  cardpred  35447  opelco3  36221  qdiffALT  37916  wl-2sb6d  38157  poimirlem26  38241  cnambfre  38263  heibor1  38405  opltn0  39910  cvrnbtwn2  39995  cvrnbtwn4  39999  atlltn0  40026  pmapjat1  40573  dih1dimatlem  42049  2rexfrabdioph  43471  dnwech  43723  rfovcnvf1od  44678  uneqsn  44699  lighneallem2  48303  stgredgiun  48668  isinito2lem  50221