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  4298  exmid01  4337  opelopabt  4406  opelopabga  4407  brabga  4408  opelopabgf  4414  elsucg  4551  elsuc2g  4552  brab2a  4830  opeliunxp  4832  posng  4849  brab2ga  4852  csbdmg  4977  elrnmpt1  5035  elrnmptg  5036  eliniseg2  5170  poleloe  5190  elxp4  5278  elxp5  5279  cnvpom  5333  sbcfung  5404  dffun8  5408  fncnv  5450  fununi  5452  fnssresb  5498  fnimaeq0  5508  funcocnv2  5667  dffn5im  5751  funimass4  5756  fnsnfv  5765  dmfco  5776  fndmdif  5817  fndmin  5819  unpreima  5836  respreima  5839  fsn2  5885  fnressn  5904  fressnfv  5905  elunirn  5975  dff13  5977  fliftel  6002  isoini  6027  f1oiso  6035  riotaeqimp  6066  acexmid  6087  fnbrovb  6133  eloprabga  6178  resoprab2  6188  ralrnmpo  6206  rexrnmpo  6207  ovid  6208  ov  6211  ovg  6231  ofrfval2  6323  fmpox  6440  1stconst  6461  2ndconst  6462  f1od2  6475  rbropapd  6517  brtpos2  6526  dfsmo2  6562  frecabcl  6674  brdifun  6838  eqerlem  6842  brecop  6903  erovlem  6905  mapfset  6949  mapsnd  6974  mapsn  6976  mptelixpg  7020  map1  7105  xpsnen  7123  xpdom2  7133  xpf1o  7148  mapunen  7155  supubti  7345  infglbti  7371  ctssdccl  7457  nninfwlpoim  7525  nninfinfwlpo  7526  netap  7626  2omotaplemap  7629  ltpiord  7692  nlt1pig  7714  elinp  7847  ltdfpr  7879  genpassl  7897  genpassu  7898  1idprl  7963  1idpru  7964  gt0srpr  8121  mappsrprg  8177  map2psrprg  8178  peano2nnnn  8226  recidpirq  8231  axprecex  8253  xrlenlt  8396  addsubeq4  8548  renegcl  8594  lesub0  8814  recexaplem2  8988  conjmulap  9067  rerecclap  9068  creui  9298  peano2nn  9325  nndiv  9354  elznn0  9670  eqreznegel  10030  negelrp  10105  ltxr  10194  divelunit  10421  iccf1o  10424  elfz2  10435  elfzp1  10496  fzdifsuc  10505  fznn  10513  nelfzo  10576  fzosplitsni  10671  fvinim0ffz  10677  infssuzex  10683  zsupssdc  10690  frec2uzisod  10865  sq11i  11087  nn0sqdc  11168  wrdval  11329  csbwrdg  11356  swrdnd  11453  wrd2ind  11517  cjreb  11653  rexfiuz  11777  cau3lem  11903  pwm1geoserap1  12300  mertensabs  12329  divides  12581  dvdsabseq  12639  odd2np1  12665  oddm1even  12667  modremain  12721  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlema  12801  bezoutlemb  12802  isprm2  12920  isprm4  12922  dvdsnprmd  12928  nnmaxpw  12978  oddprmdvds  13162  4sqlem2  13197  4sqlem12  13210  xpsfrnel2  13726  issubm  13838  grplmulf1o  13938  grplactcnv  13966  issubg  14035  elnmz  14070  isghm  14105  ghmeqker  14133  resscntz  14166  cntzsgrpcl  14167  rng1zrlem  14365  iscrng2  14426  issubrng  14616  aprval  14700  zndvds  15093  znleval  15097  psrbag  15162  istopg  15225  basgen2  15307  isnei  15370  restdis  15410  iscn  15423  iscnp  15425  lmbr2  15440  lmbrf  15441  txcn  15501  cnmpt21  15517  blres  15660  isxms2  15678  metrest  15732  metcnp  15738  txmetcnp  15744  txmetcn  15745  cnblcld  15761  reopnap  15772  sineq0re  16076  ioocosf1o  16082  mpodvdsmulf1o  16284  gausslemma2dlem0i  16381  gausslemma2dlem1a  16382  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  2lgslem1a  16412  isuhgrm  16517  isushgrm  16518  isupgren  16541  isumgren  16551  isuspgren  16603  isusgren  16604  uhgr0v0e  16680  vtxdg0v  16740  iswlk  16769  wlk1walkdom  16805  istrl  16831  clwwlkn1  16864  clwwlkn2  16867  clwwlknonel  16878  clwwlknun  16887  iseupth  16893  eupthres  16903  eupth2lem1  16904  eupth2lemsfi  16924  bj-nn0sucALT  17209  apdiff  17304  ralrals  17356  rexrals  17357  ralals  17362  rexals  17363