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 ) )

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  4608  tfis  4712  reldmm  4982  xp11m  5208  ressn  5310  fnssresb  5477  fun11iun  5642  funimass4  5734  dffo4  5832  f1ompt  5835  dfimafnf  5930  fliftf  5980  resoprab2  6160  ralrnmpo  6178  rexrnmpo  6179  1stconst  6432  2ndconst  6433  dfsmo2  6533  smoiso  6548  brecop  6874  ixpsnf1o  6986  ac6sfi  7170  ismkvnex  7461  nninfwlporlemd  7478  prarloclemn  7832  axcaucvglemres  8232  reapti  8873  indstr  9948  iccneg  10346  sqap0  10997  wrdmap  11286  wrdind  11444  sqrt00  11756  minclpr  11953  fprodseq  12300  absefib  12488  efieq1re  12489  prmind2  12848  ballotfilemsima  13209  gzsumval2  13663  eqgval  13975  isnzr2  14436  sincosq3sgn  15824  sincosq4sgn  15825  fsumdvdsmul  15990  lgsdinn0  16052  pw1nct  16918  iswomninnlem  16975