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  912  dn1dc  969  bilukdc  1441  nf4dc  1718  sbal1  2056  abbibcom  2346  abbib  2350  necon3abid  2451  necon3bid  2453  necon1abiidc  2472  r19.21t  2617  ceqsralt  2841  ceqsrexv  2947  ceqsrex2v  2949  elab2g  2964  elrabf  2971  eueq2dc  2990  euxfrdc  3003  eqreu  3009  reu8  3013  ru  3041  sbcralt  3119  sbcrext  3120  sbcne12g  3156  csbnestgf  3191  dfss4st  3454  rexsng  3730  ralprg  3740  rexprg  3741  difsn  3831  opthpr  3876  ralunsn  3902  dfiin2g  4024  iunxsng  4067  iunxsngf  4069  elpwuni  4081  pwnss  4272  exmid01  4311  opelopabt  4380  opelopabga  4381  brabga  4382  opelopabgf  4388  elsucg  4525  elsuc2g  4526  brab2a  4803  opeliunxp  4805  posng  4822  brab2ga  4825  csbdmg  4950  elrnmpt1  5008  elrnmptg  5009  eliniseg2  5142  poleloe  5162  elxp4  5250  elxp5  5251  cnvpom  5305  sbcfung  5376  dffun8  5380  fncnv  5422  fununi  5424  fnssresb  5470  fnimaeq0  5480  funcocnv2  5639  dffn5im  5722  funimass4  5727  fnsnfv  5736  dmfco  5745  fndmdif  5783  fndmin  5785  unpreima  5802  respreima  5805  fsn2  5851  fnressn  5870  fressnfv  5871  elunirn  5939  dff13  5941  fliftel  5966  isoini  5991  f1oiso  5999  riotaeqimp  6028  acexmid  6049  fnbrovb  6095  eloprabga  6140  resoprab2  6150  ralrnmpo  6168  rexrnmpo  6169  ovid  6170  ov  6173  ovg  6193  ofrfval2  6283  fmpox  6396  1stconst  6417  2ndconst  6418  f1od2  6431  rbropapd  6473  brtpos2  6482  dfsmo2  6518  frecabcl  6630  brdifun  6794  eqerlem  6798  brecop  6859  erovlem  6861  mapsnd  6923  mapsn  6925  mptelixpg  6969  map1  7054  xpsnen  7072  xpdom2  7082  xpf1o  7097  mapunen  7104  supubti  7290  infglbti  7316  ctssdccl  7402  nninfwlpoim  7470  nninfinfwlpo  7471  netap  7568  2omotaplemap  7571  ltpiord  7634  nlt1pig  7656  elinp  7789  ltdfpr  7821  genpassl  7839  genpassu  7840  1idprl  7905  1idpru  7906  gt0srpr  8063  mappsrprg  8119  map2psrprg  8120  peano2nnnn  8168  recidpirq  8173  axprecex  8195  xrlenlt  8338  addsubeq4  8488  renegcl  8534  lesub0  8753  recexaplem2  8926  conjmulap  9003  rerecclap  9004  creui  9234  peano2nn  9249  nndiv  9278  elznn0  9592  eqreznegel  9946  negelrp  10020  ltxr  10108  divelunit  10335  iccf1o  10338  elfz2  10349  elfzp1  10406  fzdifsuc  10415  fznn  10423  nelfzo  10486  fzosplitsni  10581  fvinim0ffz  10587  infssuzex  10593  zsupssdc  10598  frec2uzisod  10769  sq11i  10991  wrdval  11227  csbwrdg  11254  swrdnd  11351  wrd2ind  11415  cjreb  11551  rexfiuz  11674  cau3lem  11799  pwm1geoserap1  12194  mertensabs  12223  divides  12475  dvdsabseq  12533  odd2np1  12559  oddm1even  12561  modremain  12615  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlema  12695  bezoutlemb  12696  isprm2  12814  isprm4  12816  dvdsnprmd  12822  oddprmdvds  13052  4sqlem2  13087  4sqlem12  13100  xpsfrnel2  13559  issubm  13685  grplmulf1o  13787  grplactcnv  13815  issubg  13890  elnmz  13925  isghm  13960  ghmeqker  13988  srg1zr  14131  iscrng2  14159  issubrng  14344  aprval  14428  zndvds  14797  znleval  14801  psrbag  14817  istopg  14864  basgen2  14946  isnei  15009  restdis  15049  iscn  15062  iscnp  15064  lmbr2  15079  lmbrf  15080  txcn  15140  cnmpt21  15156  blres  15299  isxms2  15317  metrest  15371  metcnp  15377  txmetcnp  15383  txmetcn  15384  cnblcld  15400  reopnap  15411  ioocosf1o  15719  mpodvdsmulf1o  15858  gausslemma2dlem0i  15930  gausslemma2dlem1a  15931  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  2lgslem1a  15961  isuhgrm  16066  isushgrm  16067  isupgren  16090  isumgren  16100  isuspgren  16152  isusgren  16153  uhgr0v0e  16229  vtxdg0v  16289  iswlk  16318  wlk1walkdom  16354  istrl  16380  clwwlkn1  16413  clwwlkn2  16416  clwwlknonel  16427  clwwlknun  16436  iseupth  16442  eupthres  16452  eupth2lem1  16453  eupth2lemsfi  16473  bj-nn0sucALT  16748  apdiff  16832