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 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bitr3di  289  necon1abid  2995  necon4abid  2997  uniiunlem  4038  r19.9rzv  4464  2reu4lem  4482  intprg  4944  inimasn  6151  fnresdisj  6656  fnsnfv  6961  f1oiso  7355  reldm  8044  rdglim2  8424  mptelixpg  8945  1idpr  11041  nndiv  12309  fz1sbc  13657  grpid  19100  isrnghm  20583  rnghmval2  20586  znleval  21768  fbunfip  24096  lmflf  24232  metcld2  25536  lgsne0  27569  sltssnb  28032  isuvtx  29841  loopclwwlkn1b  30498  clwwlknun  30568  frgrncvvdeqlem2  30766  isph  31289  ofpreima  33125  fdifsupp  33144  ressply1mon1p  33965  eulerpartlemd  34864  bnj168  35227  cardpred  35584  opelco3  36341  qdiffALT  38067  wl-2sb6d  38308  poimirlem26  38382  cnambfre  38404  heibor1  38547  opltn0  40050  cvrnbtwn2  40135  cvrnbtwn4  40139  atlltn0  40166  pmapjat1  40713  dih1dimatlem  42189  2rexfrabdioph  43624  dnwech  43876  rfovcnvf1od  44831  uneqsn  44852  lighneallem2  48496  stgredgiun  48861  isinito2lem  50411