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  7495  nninfwlporlemd  7512  prarloclemn  7866  axcaucvglemres  8266  reapti  8909  indstr  10002  iccneg  10401  sqap0  11056  wrdmap  11350  wrdind  11508  sqrt00  11820  minclpr  12018  fprodseq  12366  absefib  12554  efieq1re  12555  prmind2  12914  ballotfilemsima  13308  gzsumval2  13763  eqgval  14075  isnzr2  14540  sincosq3sgn  15979  sincosq4sgn  15980  fsumdvdsmul  16204  ppiqub  16212  lgsdinn0  16286  pw1nct  17152  iswomninnlem  17218