Theorem bitrid 192

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

Hypotheses

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

Assertion

Ref	Expression
bitrid	|- ( ch -> ( ph <-> th ) )

Proof of Theorem bitrid

Step	Hyp	Ref	Expression
1		bitrid.1	. . 3 |- ( ph <-> ps )
2	1	a1i 9	. 2 |- ( ch -> ( ph <-> ps ) )
3		bitrid.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	bitrd 188	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:  bitr2id  193  bitr3id  194  3bitr4g  223  imim21b  253  pm5.17dc  909  dn1dc  966  bilukdc  1438  nf4dc  1716  sbal1  2053  abbi  2343  necon3abid  2439  necon3bid  2441  necon1abiidc  2460  r19.21t  2605  ceqsralt  2827  ceqsrexv  2933  ceqsrex2v  2935  elab2g  2950  elrabf  2957  eueq2dc  2976  euxfrdc  2989  eqreu  2995  reu8  2999  ru  3027  sbcralt  3105  sbcrext  3106  sbcne12g  3142  csbnestgf  3177  dfss4st  3437  rexsng  3707  ralprg  3717  rexprg  3718  difsn  3804  opthpr  3849  ralunsn  3875  dfiin2g  3997  iunxsng  4040  iunxsngf  4042  elpwuni  4054  pwnss  4242  exmid01  4281  opelopabt  4349  opelopabga  4350  brabga  4351  opelopabgf  4357  elsucg  4494  elsuc2g  4495  brab2a  4771  opeliunxp  4773  posng  4790  brab2ga  4793  csbdmg  4916  elrnmpt1  4974  elrnmptg  4975  eliniseg2  5107  poleloe  5127  elxp4  5215  elxp5  5216  cnvpom  5270  sbcfung  5341  dffun8  5345  fncnv  5386  fununi  5388  fnssresb  5434  fnimaeq0  5444  funcocnv2  5596  dffn5im  5678  funimass4  5683  fnsnfv  5692  dmfco  5701  fndmdif  5739  fndmin  5741  unpreima  5759  respreima  5762  fsn2  5808  fnressn  5824  fressnfv  5825  elunirn  5889  dff13  5891  fliftel  5916  isoini  5941  f1oiso  5949  riotaeqimp  5978  acexmid  5999  fnbrovb  6045  eloprabga  6090  resoprab2  6100  ralrnmpo  6118  rexrnmpo  6119  ovid  6120  ov  6123  ovg  6143  ofrfval2  6233  fmpox  6344  1stconst  6365  2ndconst  6366  f1od2  6379  rbropapd  6386  brtpos2  6395  dfsmo2  6431  frecabcl  6543  brdifun  6705  eqerlem  6709  brecop  6770  erovlem  6772  mapsn  6835  mptelixpg  6879  map1  6963  xpsnen  6976  xpdom2  6986  xpf1o  7001  supubti  7162  infglbti  7188  ctssdccl  7274  nninfwlpoim  7342  nninfinfwlpo  7343  netap  7436  2omotaplemap  7439  ltpiord  7502  nlt1pig  7524  elinp  7657  ltdfpr  7689  genpassl  7707  genpassu  7708  1idprl  7773  1idpru  7774  gt0srpr  7931  mappsrprg  7987  map2psrprg  7988  peano2nnnn  8036  recidpirq  8041  axprecex  8063  xrlenlt  8207  addsubeq4  8357  renegcl  8403  lesub0  8622  recexaplem2  8795  conjmulap  8872  rerecclap  8873  creui  9103  peano2nn  9118  nndiv  9147  elznn0  9457  eqreznegel  9805  negelrp  9879  ltxr  9967  divelunit  10194  iccf1o  10196  elfz2  10207  elfzp1  10264  fzdifsuc  10273  fznn  10281  nelfzo  10344  fzosplitsni  10436  fvinim0ffz  10442  infssuzex  10448  zsupssdc  10453  frec2uzisod  10624  sq11i  10846  wrdval  11069  csbwrdg  11096  swrdnd  11186  wrd2ind  11250  cjreb  11372  rexfiuz  11495  cau3lem  11620  pwm1geoserap1  12014  mertensabs  12043  divides  12295  dvdsabseq  12353  odd2np1  12379  oddm1even  12381  modremain  12435  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemmain  12514  bezoutlema  12515  bezoutlemb  12516  isprm2  12634  isprm4  12636  dvdsnprmd  12642  oddprmdvds  12872  4sqlem2  12907  4sqlem12  12920  xpsfrnel2  13374  issubm  13500  grplmulf1o  13602  grplactcnv  13630  issubg  13705  elnmz  13740  isghm  13775  ghmeqker  13803  srg1zr  13945  iscrng2  13973  issubrng  14157  aprval  14240  zndvds  14607  znleval  14611  psrbag  14627  istopg  14667  basgen2  14749  isnei  14812  restdis  14852  iscn  14865  iscnp  14867  lmbr2  14882  lmbrf  14883  txcn  14943  cnmpt21  14959  blres  15102  isxms2  15120  metrest  15174  metcnp  15180  txmetcnp  15186  txmetcn  15187  cnblcld  15203  reopnap  15214  ioocosf1o  15522  mpodvdsmulf1o  15658  gausslemma2dlem0i  15730  gausslemma2dlem1a  15731  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  2lgslem1a  15761  isuhgrm  15865  isushgrm  15866  isupgren  15889  isumgren  15899  isuspgren  15949  isusgren  15950  iswlk  16029  bj-nn0sucALT  16299  apdiff  16375