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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bitr2id  193  bitr3id  194  3bitr4g  223  imim21b  253  pm5.17dc  916  dn1dc  973  bilukdc  1445  nf4dc  1722  sbal1  2062  abbibcom  2352  abbib  2356  necon3abid  2459  necon3bid  2461  necon1abiidc  2480  r19.21t  2625  ceqsralt  2849  ceqsrexv  2956  ceqsrex2v  2958  elab2g  2973  elrabf  2980  eueq2dc  2999  euxfrdc  3012  eqreu  3018  reu8  3022  ru  3050  sbcralt  3128  sbcrext  3129  sbcne12g  3165  csbnestgf  3200  dfss4st  3464  rexsng  3750  ralprg  3760  rexprg  3761  difsn  3852  opthpr  3897  ralunsn  3923  dfiin2g  4045  iunxsng  4088  iunxsngf  4090  elpwuni  4102  pwnss  4296  exmid01  4335  opelopabt  4404  opelopabga  4405  brabga  4406  opelopabgf  4412  elsucg  4549  elsuc2g  4550  brab2a  4828  opeliunxp  4830  posng  4847  brab2ga  4850  csbdmg  4975  elrnmpt1  5033  elrnmptg  5034  eliniseg2  5167  poleloe  5187  elxp4  5275  elxp5  5276  cnvpom  5330  sbcfung  5401  dffun8  5405  fncnv  5447  fununi  5449  fnssresb  5495  fnimaeq0  5505  funcocnv2  5664  dffn5im  5748  funimass4  5753  fnsnfv  5762  dmfco  5773  fndmdif  5814  fndmin  5816  unpreima  5833  respreima  5836  fsn2  5882  fnressn  5901  fressnfv  5902  elunirn  5972  dff13  5974  fliftel  5999  isoini  6024  f1oiso  6032  riotaeqimp  6063  acexmid  6084  fnbrovb  6130  eloprabga  6175  resoprab2  6185  ralrnmpo  6203  rexrnmpo  6204  ovid  6205  ov  6208  ovg  6228  ofrfval2  6319  fmpox  6436  1stconst  6457  2ndconst  6458  f1od2  6471  rbropapd  6513  brtpos2  6522  dfsmo2  6558  frecabcl  6670  brdifun  6834  eqerlem  6838  brecop  6899  erovlem  6901  mapfset  6945  mapsnd  6970  mapsn  6972  mptelixpg  7016  map1  7101  xpsnen  7119  xpdom2  7129  xpf1o  7144  mapunen  7151  supubti  7340  infglbti  7366  ctssdccl  7452  nninfwlpoim  7520  nninfinfwlpo  7521  netap  7621  2omotaplemap  7624  ltpiord  7687  nlt1pig  7709  elinp  7842  ltdfpr  7874  genpassl  7892  genpassu  7893  1idprl  7958  1idpru  7959  gt0srpr  8116  mappsrprg  8172  map2psrprg  8173  peano2nnnn  8221  recidpirq  8226  axprecex  8248  xrlenlt  8391  addsubeq4  8543  renegcl  8589  lesub0  8809  recexaplem2  8983  conjmulap  9062  rerecclap  9063  creui  9293  peano2nn  9319  nndiv  9348  elznn0  9664  eqreznegel  10024  negelrp  10099  ltxr  10188  divelunit  10415  iccf1o  10418  elfz2  10429  elfzp1  10490  fzdifsuc  10499  fznn  10507  nelfzo  10570  fzosplitsni  10665  fvinim0ffz  10671  infssuzex  10677  zsupssdc  10684  frec2uzisod  10859  sq11i  11081  nn0sqdc  11162  wrdval  11323  csbwrdg  11350  swrdnd  11447  wrd2ind  11511  cjreb  11647  rexfiuz  11771  cau3lem  11897  pwm1geoserap1  12294  mertensabs  12323  divides  12575  dvdsabseq  12633  odd2np1  12659  oddm1even  12661  modremain  12715  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlema  12795  bezoutlemb  12796  isprm2  12914  isprm4  12916  dvdsnprmd  12922  nnmaxpw  12972  oddprmdvds  13156  4sqlem2  13191  4sqlem12  13204  xpsfrnel2  13720  issubm  13832  grplmulf1o  13932  grplactcnv  13960  issubg  14029  elnmz  14064  isghm  14099  ghmeqker  14127  resscntz  14160  cntzsgrpcl  14161  rng1zrlem  14342  iscrng2  14403  issubrng  14591  aprval  14675  zndvds  15068  znleval  15072  psrbag  15137  istopg  15191  basgen2  15273  isnei  15336  restdis  15376  iscn  15389  iscnp  15391  lmbr2  15406  lmbrf  15407  txcn  15467  cnmpt21  15483  blres  15626  isxms2  15644  metrest  15698  metcnp  15704  txmetcnp  15710  txmetcn  15711  cnblcld  15727  reopnap  15738  ioocosf1o  16047  mpodvdsmulf1o  16245  gausslemma2dlem0i  16342  gausslemma2dlem1a  16343  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem1a  16373  isuhgrm  16478  isushgrm  16479  isupgren  16502  isumgren  16512  isuspgren  16564  isusgren  16565  uhgr0v0e  16641  vtxdg0v  16701  iswlk  16730  wlk1walkdom  16766  istrl  16792  clwwlkn1  16825  clwwlkn2  16828  clwwlknonel  16839  clwwlknun  16848  iseupth  16854  eupthres  16864  eupth2lem1  16865  eupth2lemsfi  16885  bj-nn0sucALT  17170  apdiff  17264  ralrals  17316  rexrals  17317  ralals  17322  rexals  17323