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	syl5bb 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  2970  necon4abid  2972  uniiunlem  3985  r19.9rzv  4397  2reu4lem  4423  intprg  4878  inimasn  5999  fnresdisj  6475  fnsnfv  6768  f1oiso  7138  reldm  7793  rdglim2  8146  mptelixpg  8594  1idpr  10608  nndiv  11841  fz1sbc  13153  grpid  18357  znleval  20473  fbunfip  22720  lmflf  22856  metcld2  24158  lgsne0  26170  isuvtx  27437  loopclwwlkn1b  28079  clwwlknun  28149  frgrncvvdeqlem2  28337  isph  28857  ofpreima  30676  eulerpartlemd  31999  bnj168  32375  cardpred  32729  opelco3  33419  wl-2sb6d  35399  poimirlem26  35489  cnambfre  35511  heibor1  35654  opltn0  36890  cvrnbtwn2  36975  cvrnbtwn4  36979  atlltn0  37006  pmapjat1  37553  dih1dimatlem  39029  2rexfrabdioph  40262  dnwech  40517  rfovcnvf1od  41230  uneqsn  41251  lighneallem2  44674  isrnghm  45066  rnghmval2  45069