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  7339  infglbti  7365  ctssdccl  7451  nninfwlpoim  7519  nninfinfwlpo  7520  netap  7620  2omotaplemap  7623  ltpiord  7686  nlt1pig  7708  elinp  7841  ltdfpr  7873  genpassl  7891  genpassu  7892  1idprl  7957  1idpru  7958  gt0srpr  8115  mappsrprg  8171  map2psrprg  8172  peano2nnnn  8220  recidpirq  8225  axprecex  8247  xrlenlt  8390  addsubeq4  8541  renegcl  8587  lesub0  8807  recexaplem2  8980  conjmulap  9059  rerecclap  9060  creui  9290  peano2nn  9316  nndiv  9345  elznn0  9659  eqreznegel  10014  negelrp  10088  ltxr  10177  divelunit  10404  iccf1o  10407  elfz2  10418  elfzp1  10479  fzdifsuc  10488  fznn  10496  nelfzo  10559  fzosplitsni  10654  fvinim0ffz  10660  infssuzex  10666  zsupssdc  10673  frec2uzisod  10844  sq11i  11066  wrdval  11307  csbwrdg  11334  swrdnd  11431  wrd2ind  11495  cjreb  11631  rexfiuz  11755  cau3lem  11880  pwm1geoserap1  12275  mertensabs  12304  divides  12556  dvdsabseq  12614  odd2np1  12640  oddm1even  12642  modremain  12696  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlema  12776  bezoutlemb  12777  isprm2  12895  isprm4  12897  dvdsnprmd  12903  oddprmdvds  13133  4sqlem2  13168  4sqlem12  13181  xpsfrnel2  13667  issubm  13779  grplmulf1o  13879  grplactcnv  13907  issubg  13976  elnmz  14011  isghm  14046  ghmeqker  14074  rng1zrlem  14258  iscrng2  14319  issubrng  14507  aprval  14591  zndvds  14984  znleval  14988  psrbag  15053  istopg  15100  basgen2  15182  isnei  15245  restdis  15285  iscn  15298  iscnp  15300  lmbr2  15315  lmbrf  15316  txcn  15376  cnmpt21  15392  blres  15535  isxms2  15553  metrest  15607  metcnp  15613  txmetcnp  15619  txmetcn  15620  cnblcld  15636  reopnap  15647  ioocosf1o  15955  mpodvdsmulf1o  16104  gausslemma2dlem0i  16176  gausslemma2dlem1a  16177  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem1a  16207  isuhgrm  16312  isushgrm  16313  isupgren  16336  isumgren  16346  isuspgren  16398  isusgren  16399  uhgr0v0e  16475  vtxdg0v  16535  iswlk  16564  wlk1walkdom  16600  istrl  16626  clwwlkn1  16659  clwwlkn2  16662  clwwlknonel  16673  clwwlknun  16682  iseupth  16688  eupthres  16698  eupth2lem1  16699  eupth2lemsfi  16719  bj-nn0sucALT  17004  apdiff  17097  ralrals  17149  rexrals  17150  ralals  17155  rexals  17156