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 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  286  necon1abid  2982  necon4abid  2984  uniiunlem  4019  r19.9rzv  4430  2reu4lem  4456  intprg  4912  inimasn  6059  fnresdisj  6552  fnsnfv  6847  f1oiso  7222  reldm  7885  rdglim2  8263  mptelixpg  8723  1idpr  10785  nndiv  12019  fz1sbc  13332  grpid  18615  znleval  20762  fbunfip  23020  lmflf  23156  metcld2  24471  lgsne0  26483  isuvtx  27762  loopclwwlkn1b  28406  clwwlknun  28476  frgrncvvdeqlem2  28664  isph  29184  ofpreima  31002  eulerpartlemd  32333  bnj168  32709  cardpred  33062  opelco3  33749  wl-2sb6d  35713  poimirlem26  35803  cnambfre  35825  heibor1  35968  opltn0  37204  cvrnbtwn2  37289  cvrnbtwn4  37293  atlltn0  37320  pmapjat1  37867  dih1dimatlem  39343  2rexfrabdioph  40618  dnwech  40873  rfovcnvf1od  41612  uneqsn  41633  lighneallem2  45058  isrnghm  45450  rnghmval2  45453