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  4628  tfis  4732  reldmm  5002  xp11m  5229  ressn  5331  fnssresb  5498  fun11iun  5663  funimass4  5756  dffo4  5859  f1ompt  5862  dfimafnf  5958  fliftf  6008  resoprab2  6188  ralrnmpo  6206  rexrnmpo  6207  1stconst  6461  2ndconst  6462  dfsmo2  6562  smoiso  6577  brecop  6903  ixpsnf1o  7023  ac6sfi  7207  ismkvnex  7502  nninfwlporlemd  7519  prarloclemn  7873  axcaucvglemres  8273  reapti  8916  indstr  10010  iccneg  10409  sqap0  11065  wrdmap  11359  wrdind  11517  sqrt00  11829  minclpr  12028  fprodseq  12376  absefib  12564  efieq1re  12565  prmind2  12924  ballotfilemsima  13318  gzsumval2  13774  eqgval  14086  resscntz  14167  isnzr2  14601  sincosq3sgn  16067  sincosq4sgn  16068  fsumdvdsmul  16297  ppiqub  16305  lgsdinn0  16384  pw1nct  17250  iswomninnlem  17318