Theorem bitr4di 198

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

Hypotheses

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

Assertion

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

Proof of Theorem bitr4di

Step	Hyp	Ref	Expression
1		bitr4di.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		bitr4di.2	. . 3 |- ( th <-> ch )
3	2	bicomi 132	. 2 |- ( ch <-> th )
4	1, 3	bitrdi 196	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:  3bitr4g  223  bibi2i  227  3bior1fd  1389  3biant1d  1392  equsalh  1774  eueq3dc  2991  sbcel12g  3153  sbceqg  3154  sbcnel12g  3155  reldisj  3560  r19.3rm  3598  eldifpr  3716  eldiftp  3735  rabxp  4787  elrng  4946  iss  5084  eliniseg  5132  fcnvres  5550  dffv3g  5666  funimass4  5727  fndmdif  5783  fneqeql  5786  funimass3  5794  elrnrexdmb  5817  dff4im  5823  fconst4m  5904  elunirn  5939  riota1  6023  riota2df  6025  f1ocnvfv3  6039  eqfnov  6160  caoftrn  6299  suppimacnvfn  6446  suppssrst  6461  suppssrgst  6462  mpoxopovel  6472  rntpos  6488  ordgt0ge1  6668  iinerm  6841  erinxp  6843  qliftfun  6851  mapdm0  6897  elfi2  7259  fifo  7267  2omap  7269  inl11  7356  ctssdccl  7402  isomnimap  7428  ismkvmap  7445  iswomnimap  7457  omniwomnimkv  7458  pr2nelem  7488  indpi  7657  genpdflem  7822  genpdisj  7838  genpassl  7839  genpassu  7840  ltnqpri  7909  ltpopr  7910  ltexprlemm  7915  ltexprlemdisj  7921  ltexprlemloc  7922  ltrennb  8169  letri3  8354  letr  8356  ltneg  8736  leneg  8739  reapltxor  8863  apsym  8880  suprnubex  9227  suprleubex  9228  elnnnn0  9539  fcdmnn0fsupp  9549  zrevaddcl  9628  znnsub  9629  znn0sub  9643  prime  9677  eluz2  9859  eluz2b1  9933  nn01to3  9949  qrevaddcl  9976  xrletri3  10137  xrletr  10141  iccid  10258  elicopnf  10302  fzsplit2  10384  fzsn  10400  fzpr  10411  uzsplit  10426  fvinim0ffz  10587  lt2sqi  10989  le2sqi  10990  sseqn  11203  ccatlcan  11410  ccatrcan  11411  abs00ap  11747  iooinsup  11962  mertenslem2  12222  fprod2dlemstep  12308  gcddiv  12715  algcvgblem  12746  isprm3  12815  dvdsfi  12936  imasmnd2  13665  imasgrp2  13827  issubg  13890  resgrpisgrp  13912  eqgval  13940  imasrng  14100  ring1  14203  imasring  14208  crngunit  14256  lssle0  14520  lssats2  14562  zndvds  14797  znleval  14801  znleval2  14802  eltg2b  14919  discld  15001  opnssneib  15021  restbasg  15033  ssidcn  15075  cnptoprest2  15105  lmss  15111  txrest  15141  txlm  15144  imasnopn  15164  bldisj  15266  xmeter  15301  bl2ioo  15415  limcdifap  15527  issubgr  16252  bj-sseq  16564  nnti  16766  pw1nct  16777