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  908  baib  931  pm5.6dc  938  ifptru  1002  ifpfal  1003  xornbidc  1440  mo2dc  2142  reu8  3022  sbc6g  3076  dfss4st  3464  r19.28m  3617  r19.45mv  3621  r19.44mv  3622  r19.27m  3623  ralsnsg  3745  ralsns  3746  eldifvsn  3845  iunconstm  4018  iinconstm  4019  exmidsssnc  4338  unisucg  4557  relsng  4876  funssres  5418  fncnv  5445  dff1o5  5646  funimass4  5750  fneqeql2  5812  fnniniseg2  5826  unpreima  5827  dffo3  5849  funfvima  5944  dff13  5968  f1eqcocnv  5991  fliftf  5999  isocnv2  6012  eloprabga  6169  mpo2eqb  6192  opabex3d  6344  opabex3  6345  elxp6  6397  elxp7  6398  mptsuppd  6490  sbthlemi5  7272  sbthlemi6  7273  nninfwlporlemd  7506  genpdflem  7868  ltnqpr  7954  ltexprlemloc  7968  xrlenlt  8384  negcon2  8573  dfinfre  9280  sup3exmid  9281  elznn  9643  zq  10009  rpnegap  10070  infssuzex  10649  modqmuladdnn0  10788  shftdm  11570  rexfiuz  11738  rexanuz2  11740  sumsplitdc  12182  fsum2dlemstep  12184  odd2np1  12623  divalgb  12675  nninfctlemfo  12800  isprm4  12880  ctiunctlemudc  13311  grp1  13894  nmznsg  13999  qusecsub  14118  iscrng2  14302  opprsubgg  14373  opprsubrngg  14502  domnmuln0  14565  ringunitsap0  14577  drnguiap  14592  tx1cn  15353  tx2cn  15354  cnbl0  15618  cnblcld  15619  reopnap  15630  pilem1  15863  sinq34lt0t  15915  birthdaylem3  16072  gausslemma2dlem1a  16160  vtxd0nedgbfi  16523