Theorem bitr3id 194

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

Hypotheses

Ref	Expression
bitr3id.1	|- ( ps <-> ph )
bitr3id.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
bitr3id	|- ( ch -> ( ph <-> th ) )

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 132	. 2 |- ( ph <-> ps )
3		bitr3id.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	bitrid 192	1 |- ( ch -> ( ph <-> th ) )

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  11057  wrdmap  11351  wrdind  11509  sqrt00  11821  minclpr  12020  fprodseq  12368  absefib  12556  efieq1re  12557  prmind2  12916  ballotfilemsima  13310  gzsumval2  13765  eqgval  14077  isnzr2  14542  sincosq3sgn  15982  sincosq4sgn  15983  fsumdvdsmul  16207  ppiqub  16215  lgsdinn0  16289  pw1nct  17155  iswomninnlem  17221