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  907  19.16  1604  19.19  1714  cbvab  2360  necon1bbiidc  2475  rspc2gv  2936  elabgt  2961  sbceq1a  3055  sbcralt  3122  sbcrext  3123  sbccsbg  3170  sbccsb2g  3171  iunpw  4606  tfis  4710  reldmm  4980  xp11m  5206  ressn  5308  fnssresb  5475  fun11iun  5640  funimass4  5732  dffo4  5830  f1ompt  5833  dfimafnf  5928  fliftf  5978  resoprab2  6158  ralrnmpo  6176  rexrnmpo  6177  1stconst  6430  2ndconst  6431  dfsmo2  6531  smoiso  6546  brecop  6872  ixpsnf1o  6984  ac6sfi  7168  ismkvnex  7459  nninfwlporlemd  7476  prarloclemn  7830  axcaucvglemres  8230  reapti  8871  indstr  9946  iccneg  10344  sqap0  10995  wrdmap  11284  wrdind  11442  sqrt00  11753  minclpr  11950  fprodseq  12297  absefib  12485  efieq1re  12486  prmind2  12845  ballotfilemsima  13206  gsumval2  13663  eqgval  13979  isnzr2  14432  sincosq3sgn  15822  sincosq4sgn  15823  fsumdvdsmul  15988  lgsdinn0  16050  pw1nct  16916  iswomninnlem  16973