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  905  dn1dc  962  bilukdc  1407  nf4dc  1681  sbal1  2018  abbi  2307  necon3abid  2403  necon3bid  2405  necon1abiidc  2424  r19.21t  2569  ceqsralt  2787  ceqsrexv  2891  ceqsrex2v  2893  elab2g  2908  elrabf  2915  eueq2dc  2934  euxfrdc  2947  eqreu  2953  reu8  2957  ru  2985  sbcralt  3063  sbcrext  3064  sbcne12g  3099  csbnestgf  3134  dfss4st  3393  rexsng  3660  ralprg  3670  rexprg  3671  difsn  3756  opthpr  3799  ralunsn  3824  dfiin2g  3946  iunxsng  3989  iunxsngf  3991  elpwuni  4003  pwnss  4189  exmid01  4228  opelopabt  4293  opelopabga  4294  brabga  4295  opelopabgf  4301  elsucg  4436  elsuc2g  4437  brab2a  4713  opeliunxp  4715  posng  4732  brab2ga  4735  csbdmg  4857  elrnmpt1  4914  elrnmptg  4915  eliniseg2  5046  poleloe  5066  elxp4  5154  elxp5  5155  cnvpom  5209  sbcfung  5279  dffun8  5283  fncnv  5321  fununi  5323  fnssresb  5367  fnimaeq0  5376  funcocnv2  5526  dffn5im  5603  funimass4  5608  fnsnfv  5617  dmfco  5626  fndmdif  5664  fndmin  5666  unpreima  5684  respreima  5687  fsn2  5733  fnressn  5745  fressnfv  5746  elunirn  5810  dff13  5812  fliftel  5837  isoini  5862  f1oiso  5870  acexmid  5918  eloprabga  6006  resoprab2  6016  ralrnmpo  6034  rexrnmpo  6035  ovid  6036  ov  6039  ovg  6059  ofrfval2  6149  fmpox  6255  1stconst  6276  2ndconst  6277  f1od2  6290  rbropapd  6297  brtpos2  6306  dfsmo2  6342  frecabcl  6454  brdifun  6616  eqerlem  6620  brecop  6681  erovlem  6683  mapsn  6746  mptelixpg  6790  map1  6868  xpsnen  6877  xpdom2  6887  xpf1o  6902  supubti  7060  infglbti  7086  ctssdccl  7172  nninfwlpoim  7239  netap  7316  2omotaplemap  7319  ltpiord  7381  nlt1pig  7403  elinp  7536  ltdfpr  7568  genpassl  7586  genpassu  7587  1idprl  7652  1idpru  7653  gt0srpr  7810  mappsrprg  7866  map2psrprg  7867  peano2nnnn  7915  recidpirq  7920  axprecex  7942  xrlenlt  8086  addsubeq4  8236  renegcl  8282  lesub0  8500  recexaplem2  8673  conjmulap  8750  rerecclap  8751  creui  8981  peano2nn  8996  nndiv  9025  elznn0  9335  eqreznegel  9682  negelrp  9756  ltxr  9844  divelunit  10071  iccf1o  10073  elfz2  10084  elfzp1  10141  fzdifsuc  10150  fznn  10158  nelfzo  10221  fzosplitsni  10305  fvinim0ffz  10311  frec2uzisod  10481  sq11i  10703  wrdval  10920  csbwrdg  10946  cjreb  11013  rexfiuz  11136  cau3lem  11261  pwm1geoserap1  11654  mertensabs  11683  divides  11935  dvdsabseq  11992  odd2np1  12017  oddm1even  12019  modremain  12073  infssuzex  12089  zsupssdc  12094  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlema  12139  bezoutlemb  12140  isprm2  12258  isprm4  12260  dvdsnprmd  12266  oddprmdvds  12495  4sqlem2  12530  4sqlem12  12543  xpsfrnel2  12932  issubm  13047  grplmulf1o  13149  grplactcnv  13177  issubg  13246  elnmz  13281  isghm  13316  ghmeqker  13344  srg1zr  13486  iscrng2  13514  issubrng  13698  aprval  13781  zndvds  14148  znleval  14152  psrbag  14166  istopg  14178  basgen2  14260  isnei  14323  restdis  14363  iscn  14376  iscnp  14378  lmbr2  14393  lmbrf  14394  txcn  14454  cnmpt21  14470  blres  14613  isxms2  14631  metrest  14685  metcnp  14691  txmetcnp  14697  txmetcn  14698  cnblcld  14714  reopnap  14725  ioocosf1o  15030  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem1a  15245  bj-nn0sucALT  15540  apdiff  15608