Theorem bitr4id 199

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

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

Assertion

Ref	Expression
bitr4id	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitr4id

Step	Hyp	Ref	Expression
1		bitr4id.1	. 2 |- ( ph -> ( th <-> ch ) )
2		bitr4id.2	. . 3 |- ( ps <-> ch )
3	2	bicomi 132	. 2 |- ( ch <-> ps )
4	1, 3	bitr2di 197	1 |- ( ph -> ( ps <-> 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:  imimorbdc  897  baib  920  pm5.6dc  927  xornbidc  1402  mo2dc  2097  reu8  2956  sbc6g  3010  dfss4st  3392  r19.28m  3536  r19.45mv  3540  r19.44mv  3541  r19.27m  3542  ralsnsg  3655  ralsns  3656  iunconstm  3920  iinconstm  3921  exmidsssnc  4232  unisucg  4445  relsng  4762  funssres  5296  fncnv  5320  dff1o5  5509  funimass4  5607  fneqeql2  5667  fnniniseg2  5681  rexsupp  5682  unpreima  5683  dffo3  5705  funfvima  5790  dff13  5811  f1eqcocnv  5834  fliftf  5842  isocnv2  5855  eloprabga  6005  mpo2eqb  6028  opabex3d  6173  opabex3  6174  elxp6  6222  elxp7  6223  sbthlemi5  7020  sbthlemi6  7021  nninfwlporlemd  7231  genpdflem  7567  ltnqpr  7653  ltexprlemloc  7667  xrlenlt  8084  negcon2  8272  dfinfre  8975  sup3exmid  8976  elznn  9333  zq  9691  rpnegap  9752  modqmuladdnn0  10439  shftdm  10966  rexfiuz  11133  rexanuz2  11135  sumsplitdc  11575  fsum2dlemstep  11577  odd2np1  12014  divalgb  12066  infssuzex  12086  nninfctlemfo  12177  isprm4  12257  ctiunctlemudc  12594  grp1  13178  nmznsg  13283  qusecsub  13401  iscrng2  13511  opprsubgg  13580  opprsubrngg  13707  domnmuln0  13769  tx1cn  14437  tx2cn  14438  cnbl0  14702  cnblcld  14703  reopnap  14706  pilem1  14914  sinq34lt0t  14966  gausslemma2dlem1a  15174