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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitr3g  222  imbibi  252  ianordc  911  19.16  1608  19.19  1718  cbvab  2364  necon1bbiidc  2481  rspc2gv  2942  elabgt  2967  sbceq1a  3061  sbcralt  3128  sbcrext  3129  sbccsbg  3176  sbccsb2g  3177  iunpw  4626  tfis  4730  reldmm  5000  xp11m  5226  ressn  5328  fnssresb  5495  fun11iun  5660  funimass4  5753  dffo4  5856  f1ompt  5859  dfimafnf  5955  fliftf  6005  resoprab2  6185  ralrnmpo  6203  rexrnmpo  6204  1stconst  6457  2ndconst  6458  dfsmo2  6558  smoiso  6573  brecop  6899  ixpsnf1o  7018  ac6sfi  7202  ismkvnex  7496  nninfwlporlemd  7513  prarloclemn  7867  axcaucvglemres  8267  reapti  8910  indstr  10003  iccneg  10402  sqap0  11058  wrdmap  11352  wrdind  11510  sqrt00  11822  minclpr  12021  fprodseq  12369  absefib  12557  efieq1re  12558  prmind2  12917  ballotfilemsima  13311  gzsumval2  13767  eqgval  14079  resscntz  14160  isnzr2  14575  sincosq3sgn  16021  sincosq4sgn  16022  fsumdvdsmul  16251  ppiqub  16259  lgsdinn0  16338  pw1nct  17204  iswomninnlem  17271