Theorem bitr3id 194

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3id.1	⊢ (𝜓 ↔ 𝜑)
bitr3id.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
bitr3id	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 132	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrid 192	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr3g  222  imbibi  252  ianordc  900  19.16  1569  19.19  1680  cbvab  2320  necon1bbiidc  2428  rspc2gv  2880  elabgt  2905  sbceq1a  2999  sbcralt  3066  sbcrext  3067  sbccsbg  3113  sbccsb2g  3114  iunpw  4516  tfis  4620  xp11m  5109  ressn  5211  fnssresb  5373  fun11iun  5528  funimass4  5614  dffo4  5713  f1ompt  5716  fliftf  5849  resoprab2  6023  ralrnmpo  6041  rexrnmpo  6042  1stconst  6288  2ndconst  6289  dfsmo2  6354  smoiso  6369  brecop  6693  ixpsnf1o  6804  ac6sfi  6968  ismkvnex  7230  nninfwlporlemd  7247  prarloclemn  7585  axcaucvglemres  7985  reapti  8625  indstr  9686  iccneg  10083  sqap0  10717  wrdmap  10985  sqrt00  11224  minclpr  11421  fprodseq  11767  absefib  11955  efieq1re  11956  prmind2  12315  gsumval2  13101  eqgval  13431  isnzr2  13818  sincosq3sgn  15150  sincosq4sgn  15151  fsumdvdsmul  15313  lgsdinn0  15375  pw1nct  15736  iswomninnlem  15784