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  901  baib  924  pm5.6dc  931  ifptru  995  ifpfal  996  xornbidc  1433  mo2dc  2133  reu8  2999  sbc6g  3053  dfss4st  3437  r19.28m  3581  r19.45mv  3585  r19.44mv  3586  r19.27m  3587  ralsnsg  3703  ralsns  3704  iunconstm  3973  iinconstm  3974  exmidsssnc  4287  unisucg  4505  relsng  4822  funssres  5360  fncnv  5387  dff1o5  5581  funimass4  5684  fneqeql2  5744  fnniniseg2  5758  rexsupp  5759  unpreima  5760  dffo3  5782  funfvima  5871  dff13  5892  f1eqcocnv  5915  fliftf  5923  isocnv2  5936  eloprabga  6091  mpo2eqb  6114  opabex3d  6266  opabex3  6267  elxp6  6315  elxp7  6316  sbthlemi5  7128  sbthlemi6  7129  nninfwlporlemd  7339  genpdflem  7694  ltnqpr  7780  ltexprlemloc  7794  xrlenlt  8211  negcon2  8399  dfinfre  9103  sup3exmid  9104  elznn  9462  zq  9821  rpnegap  9882  infssuzex  10453  modqmuladdnn0  10590  shftdm  11333  rexfiuz  11500  rexanuz2  11502  sumsplitdc  11943  fsum2dlemstep  11945  odd2np1  12384  divalgb  12436  nninfctlemfo  12561  isprm4  12641  ctiunctlemudc  13008  grp1  13639  nmznsg  13750  qusecsub  13868  iscrng2  13978  opprsubgg  14047  opprsubrngg  14175  domnmuln0  14237  tx1cn  14943  tx2cn  14944  cnbl0  15208  cnblcld  15209  reopnap  15220  pilem1  15453  sinq34lt0t  15505  gausslemma2dlem1a  15737