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  3805  opthpr  3850  ralunsn  3876  dfiin2g  3998  iunxsng  4041  iunxsngf  4043  elpwuni  4055  pwnss  4243  exmid01  4282  opelopabt  4350  opelopabga  4351  brabga  4352  opelopabgf  4358  elsucg  4495  elsuc2g  4496  brab2a  4772  opeliunxp  4774  posng  4791  brab2ga  4794  csbdmg  4917  elrnmpt1  4975  elrnmptg  4976  eliniseg2  5108  poleloe  5128  elxp4  5216  elxp5  5217  cnvpom  5271  sbcfung  5342  dffun8  5346  fncnv  5387  fununi  5389  fnssresb  5435  fnimaeq0  5445  funcocnv2  5599  dffn5im  5681  funimass4  5686  fnsnfv  5695  dmfco  5704  fndmdif  5742  fndmin  5744  unpreima  5762  respreima  5765  fsn2  5811  fnressn  5829  fressnfv  5830  elunirn  5896  dff13  5898  fliftel  5923  isoini  5948  f1oiso  5956  riotaeqimp  5985  acexmid  6006  fnbrovb  6052  eloprabga  6097  resoprab2  6107  ralrnmpo  6125  rexrnmpo  6126  ovid  6127  ov  6130  ovg  6150  ofrfval2  6241  fmpox  6352  1stconst  6373  2ndconst  6374  f1od2  6387  rbropapd  6394  brtpos2  6403  dfsmo2  6439  frecabcl  6551  brdifun  6715  eqerlem  6719  brecop  6780  erovlem  6782  mapsn  6845  mptelixpg  6889  map1  6973  xpsnen  6988  xpdom2  6998  xpf1o  7013  supubti  7177  infglbti  7203  ctssdccl  7289  nninfwlpoim  7357  nninfinfwlpo  7358  netap  7451  2omotaplemap  7454  ltpiord  7517  nlt1pig  7539  elinp  7672  ltdfpr  7704  genpassl  7722  genpassu  7723  1idprl  7788  1idpru  7789  gt0srpr  7946  mappsrprg  8002  map2psrprg  8003  peano2nnnn  8051  recidpirq  8056  axprecex  8078  xrlenlt  8222  addsubeq4  8372  renegcl  8418  lesub0  8637  recexaplem2  8810  conjmulap  8887  rerecclap  8888  creui  9118  peano2nn  9133  nndiv  9162  elznn0  9472  eqreznegel  9821  negelrp  9895  ltxr  9983  divelunit  10210  iccf1o  10212  elfz2  10223  elfzp1  10280  fzdifsuc  10289  fznn  10297  nelfzo  10360  fzosplitsni  10453  fvinim0ffz  10459  infssuzex  10465  zsupssdc  10470  frec2uzisod  10641  sq11i  10863  wrdval  11087  csbwrdg  11114  swrdnd  11206  wrd2ind  11270  cjreb  11392  rexfiuz  11515  cau3lem  11640  pwm1geoserap1  12034  mertensabs  12063  divides  12315  dvdsabseq  12373  odd2np1  12399  oddm1even  12401  modremain  12455  bezoutlemnewy  12532  bezoutlemstep  12533  bezoutlemmain  12534  bezoutlema  12535  bezoutlemb  12536  isprm2  12654  isprm4  12656  dvdsnprmd  12662  oddprmdvds  12892  4sqlem2  12927  4sqlem12  12940  xpsfrnel2  13394  issubm  13520  grplmulf1o  13622  grplactcnv  13650  issubg  13725  elnmz  13760  isghm  13795  ghmeqker  13823  srg1zr  13965  iscrng2  13993  issubrng  14178  aprval  14261  zndvds  14628  znleval  14632  psrbag  14648  istopg  14688  basgen2  14770  isnei  14833  restdis  14873  iscn  14886  iscnp  14888  lmbr2  14903  lmbrf  14904  txcn  14964  cnmpt21  14980  blres  15123  isxms2  15141  metrest  15195  metcnp  15201  txmetcnp  15207  txmetcn  15208  cnblcld  15224  reopnap  15235  ioocosf1o  15543  mpodvdsmulf1o  15679  gausslemma2dlem0i  15751  gausslemma2dlem1a  15752  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  2lgslem1a  15782  isuhgrm  15886  isushgrm  15887  isupgren  15910  isumgren  15920  isuspgren  15970  isusgren  15971  vtxdg0v  16053  iswlk  16064  wlk1walkdom  16100  istrl  16124  bj-nn0sucALT  16396  apdiff  16476