Theorem bitrid 191

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 187	1 |- ( ch -> ( ph <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr2id  192  bitr3id  193  3bitr4g  222  imim21b  251  pm5.17dc  900  dn1dc  956  bilukdc  1392  nf4dc  1664  sbal1  1996  abbi  2285  necon3abid  2380  necon3bid  2382  necon1abiidc  2401  r19.21t  2546  ceqsralt  2758  ceqsrexv  2861  ceqsrex2v  2863  elab2g  2878  elrabf  2885  eueq2dc  2904  euxfrdc  2917  eqreu  2923  reu8  2927  ru  2955  sbcralt  3032  sbcrext  3033  sbcne12g  3068  csbnestgf  3102  dfss4st  3361  rexsng  3625  ralprg  3635  rexprg  3636  difsn  3718  opthpr  3760  ralunsn  3785  dfiin2g  3907  iunxsng  3949  iunxsngf  3951  elpwuni  3963  pwnss  4146  exmid01  4185  opelopabt  4248  opelopabga  4249  brabga  4250  elsucg  4390  elsuc2g  4391  brab2a  4665  opeliunxp  4667  posng  4684  brab2ga  4687  csbdmg  4806  elrnmpt1  4863  elrnmptg  4864  poleloe  5012  elxp4  5100  elxp5  5101  cnvpom  5155  sbcfung  5224  dffun8  5228  fncnv  5266  fununi  5268  fnssresb  5312  fnimaeq0  5321  funcocnv2  5470  dffn5im  5545  funimass4  5550  fnsnfv  5559  dmfco  5568  fndmdif  5605  fndmin  5607  unpreima  5625  respreima  5628  fsn2  5674  fnressn  5686  fressnfv  5687  elunirn  5749  dff13  5751  fliftel  5776  isoini  5801  f1oiso  5809  acexmid  5856  eloprabga  5944  resoprab2  5954  ralrnmpo  5971  rexrnmpo  5972  ovid  5973  ov  5976  ovg  5995  ofrfval2  6081  fmpox  6183  1stconst  6204  2ndconst  6205  f1od2  6218  rbropapd  6225  brtpos2  6234  dfsmo2  6270  frecabcl  6382  brdifun  6544  eqerlem  6548  brecop  6607  erovlem  6609  mapsn  6672  mptelixpg  6716  map1  6794  xpsnen  6803  xpdom2  6813  xpf1o  6826  supubti  6980  infglbti  7006  ctssdccl  7092  nninfwlpoim  7158  ltpiord  7285  nlt1pig  7307  elinp  7440  ltdfpr  7472  genpassl  7490  genpassu  7491  1idprl  7556  1idpru  7557  gt0srpr  7714  mappsrprg  7770  map2psrprg  7771  peano2nnnn  7819  recidpirq  7824  axprecex  7846  xrlenlt  7988  addsubeq4  8138  renegcl  8184  lesub0  8402  recexaplem2  8574  conjmulap  8650  rerecclap  8651  creui  8880  peano2nn  8894  nndiv  8923  elznn0  9231  eqreznegel  9577  negelrp  9648  ltxr  9736  divelunit  9963  iccf1o  9965  elfz2  9976  elfzp1  10032  fzdifsuc  10041  fznn  10049  fzosplitsni  10195  fvinim0ffz  10201  frec2uzisod  10367  sq11i  10569  cjreb  10834  rexfiuz  10957  cau3lem  11082  pwm1geoserap1  11475  mertensabs  11504  divides  11755  dvdsabseq  11811  odd2np1  11836  oddm1even  11838  modremain  11892  infssuzex  11908  zsupssdc  11913  bezoutlemnewy  11955  bezoutlemstep  11956  bezoutlemmain  11957  bezoutlema  11958  bezoutlemb  11959  isprm2  12075  isprm4  12077  dvdsnprmd  12083  oddprmdvds  12310  4sqlem2  12345  issubm  12717  grplmulf1o  12795  grplactcnv  12823  istopg  12908  basgen2  12992  isnei  13055  restdis  13095  iscn  13108  iscnp  13110  lmbr2  13125  lmbrf  13126  txcn  13186  cnmpt21  13202  blres  13345  isxms2  13363  metrest  13417  metcnp  13423  txmetcnp  13429  txmetcn  13430  cnblcld  13446  reopnap  13449  ioocosf1o  13686  bj-nn0sucALT  14130  apdiff  14197