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  2997  necon4abid  2999  uniiunlem  4015  r19.9rzv  4464  2reu4lem  4482  intprg  4944  inimasn  6158  fnresdisj  6681  fnsnfv  6987  f1oiso  7382  reldmOLD  8080  rdglim2  8468  mptelixpg  8991  1idpr  11141  nndiv  12411  fz1sbc  13761  grpid  19215  isrnghm  20701  rnghmval2  20704  znleval  21890  fbunfip  24218  lmflf  24354  metcld2  25658  lgsne0  27692  sltssnb  28185  isuvtx  30006  loopclwwlkn1b  30663  clwwlknun  30733  frgrncvvdeqlem2  30931  isph  31454  ofpreima  33331  fdifsupp  33349  ressply1mon1p  34170  eulerpartlemd  35068  bnj168  35431  cardpred  35805  opelco3  36717  qdiffALT  38441  wl-2sb6d  38682  poimirlem26  38756  cnambfre  38778  heibor1  38936  opltn0  40439  cvrnbtwn2  40524  cvrnbtwn4  40528  atlltn0  40555  pmapjat1  41102  dih1dimatlem  42578  2rexfrabdioph  43996  dnwech  44248  rfovcnvf1od  45196  uneqsn  45217  lighneallem2  48896  stgredgiun  49261  isinito2lem  50838