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  2828  ceqsrexv  2934  ceqsrex2v  2936  elab2g  2951  elrabf  2958  eueq2dc  2977  euxfrdc  2990  eqreu  2996  reu8  3000  ru  3028  sbcralt  3106  sbcrext  3107  sbcne12g  3143  csbnestgf  3178  dfss4st  3438  rexsng  3708  ralprg  3718  rexprg  3719  difsn  3808  opthpr  3853  ralunsn  3879  dfiin2g  4001  iunxsng  4044  iunxsngf  4046  elpwuni  4058  pwnss  4247  exmid01  4286  opelopabt  4354  opelopabga  4355  brabga  4356  opelopabgf  4362  elsucg  4499  elsuc2g  4500  brab2a  4777  opeliunxp  4779  posng  4796  brab2ga  4799  csbdmg  4923  elrnmpt1  4981  elrnmptg  4982  eliniseg2  5114  poleloe  5134  elxp4  5222  elxp5  5223  cnvpom  5277  sbcfung  5348  dffun8  5352  fncnv  5393  fununi  5395  fnssresb  5441  fnimaeq0  5451  funcocnv2  5605  dffn5im  5687  funimass4  5692  fnsnfv  5701  dmfco  5710  fndmdif  5748  fndmin  5750  unpreima  5768  respreima  5771  fsn2  5817  fnressn  5835  fressnfv  5836  elunirn  5902  dff13  5904  fliftel  5929  isoini  5954  f1oiso  5962  riotaeqimp  5991  acexmid  6012  fnbrovb  6058  eloprabga  6103  resoprab2  6113  ralrnmpo  6131  rexrnmpo  6132  ovid  6133  ov  6136  ovg  6156  ofrfval2  6247  fmpox  6360  1stconst  6381  2ndconst  6382  f1od2  6395  rbropapd  6403  brtpos2  6412  dfsmo2  6448  frecabcl  6560  brdifun  6724  eqerlem  6728  brecop  6789  erovlem  6791  mapsn  6854  mptelixpg  6898  map1  6982  xpsnen  7000  xpdom2  7010  xpf1o  7025  supubti  7189  infglbti  7215  ctssdccl  7301  nninfwlpoim  7369  nninfinfwlpo  7370  netap  7463  2omotaplemap  7466  ltpiord  7529  nlt1pig  7551  elinp  7684  ltdfpr  7716  genpassl  7734  genpassu  7735  1idprl  7800  1idpru  7801  gt0srpr  7958  mappsrprg  8014  map2psrprg  8015  peano2nnnn  8063  recidpirq  8068  axprecex  8090  xrlenlt  8234  addsubeq4  8384  renegcl  8430  lesub0  8649  recexaplem2  8822  conjmulap  8899  rerecclap  8900  creui  9130  peano2nn  9145  nndiv  9174  elznn0  9484  eqreznegel  9838  negelrp  9912  ltxr  10000  divelunit  10227  iccf1o  10229  elfz2  10240  elfzp1  10297  fzdifsuc  10306  fznn  10314  nelfzo  10377  fzosplitsni  10471  fvinim0ffz  10477  infssuzex  10483  zsupssdc  10488  frec2uzisod  10659  sq11i  10881  wrdval  11106  csbwrdg  11133  swrdnd  11230  wrd2ind  11294  cjreb  11417  rexfiuz  11540  cau3lem  11665  pwm1geoserap1  12059  mertensabs  12088  divides  12340  dvdsabseq  12398  odd2np1  12424  oddm1even  12426  modremain  12480  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlema  12560  bezoutlemb  12561  isprm2  12679  isprm4  12681  dvdsnprmd  12687  oddprmdvds  12917  4sqlem2  12952  4sqlem12  12965  xpsfrnel2  13419  issubm  13545  grplmulf1o  13647  grplactcnv  13675  issubg  13750  elnmz  13785  isghm  13820  ghmeqker  13848  srg1zr  13990  iscrng2  14018  issubrng  14203  aprval  14286  zndvds  14653  znleval  14657  psrbag  14673  istopg  14713  basgen2  14795  isnei  14858  restdis  14898  iscn  14911  iscnp  14913  lmbr2  14928  lmbrf  14929  txcn  14989  cnmpt21  15005  blres  15148  isxms2  15166  metrest  15220  metcnp  15226  txmetcnp  15232  txmetcn  15233  cnblcld  15249  reopnap  15260  ioocosf1o  15568  mpodvdsmulf1o  15704  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem1a  15807  isuhgrm  15912  isushgrm  15913  isupgren  15936  isumgren  15946  isuspgren  15996  isusgren  15997  uhgr0v0e  16073  vtxdg0v  16100  iswlk  16120  wlk1walkdom  16156  istrl  16180  clwwlkn1  16213  clwwlkn2  16216  clwwlknonel  16227  clwwlknun  16236  iseupth  16242  eupthres  16252  bj-nn0sucALT  16509  apdiff  16588