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  2993  necon4abid  2995  uniiunlem  4012  r19.9rzv  4460  2reu4lem  4478  intprg  4940  inimasn  6145  fnresdisj  6659  fnsnfv  6964  f1oiso  7359  reldm  8055  rdglim2  8440  mptelixpg  8963  1idpr  11114  nndiv  12384  fz1sbc  13734  grpid  19186  isrnghm  20671  rnghmval2  20674  znleval  21860  fbunfip  24188  lmflf  24324  metcld2  25628  lgsne0  27662  sltssnb  28155  isuvtx  29976  loopclwwlkn1b  30633  clwwlknun  30703  frgrncvvdeqlem2  30901  isph  31424  ofpreima  33301  fdifsupp  33320  ressply1mon1p  34142  eulerpartlemd  35040  bnj168  35403  cardpred  35763  opelco3  36581  qdiffALT  38292  wl-2sb6d  38533  poimirlem26  38607  cnambfre  38629  heibor1  38787  opltn0  40290  cvrnbtwn2  40375  cvrnbtwn4  40379  atlltn0  40406  pmapjat1  40953  dih1dimatlem  42429  2rexfrabdioph  43846  dnwech  44098  rfovcnvf1od  45047  uneqsn  45068  lighneallem2  48734  stgredgiun  49099  isinito2lem  50649