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  2971  necon4abid  2973  uniiunlem  4028  r19.9rzv  4446  2reu4lem  4464  intprg  4924  inimasn  6121  fnresdisj  6619  fnsnfv  6920  f1oiso  7306  reldm  7997  rdglim2  8371  mptelixpg  8883  1idpr  10952  nndiv  12223  fz1sbc  13554  grpid  18951  isrnghm  20421  rnghmval2  20424  znleval  21534  fbunfip  23834  lmflf  23970  metcld2  25274  lgsne0  27298  sltssnb  27761  isuvtx  29464  loopclwwlkn1b  30112  clwwlknun  30182  frgrncvvdeqlem2  30370  isph  30893  ofpreima  32738  fdifsupp  32758  ressply1mon1p  33628  eulerpartlemd  34510  bnj168  34873  cardpred  35235  opelco3  35957  qdiffALT  37642  wl-2sb6d  37883  poimirlem26  37967  cnambfre  37989  heibor1  38131  opltn0  39636  cvrnbtwn2  39721  cvrnbtwn4  39725  atlltn0  39752  pmapjat1  40299  dih1dimatlem  41775  2rexfrabdioph  43224  dnwech  43476  rfovcnvf1od  44431  uneqsn  44452  lighneallem2  48063  stgredgiun  48428  isinito2lem  49967