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  1684  sbal1  2021  abbi  2310  necon3abid  2406  necon3bid  2408  necon1abiidc  2427  r19.21t  2572  ceqsralt  2790  ceqsrexv  2894  ceqsrex2v  2896  elab2g  2911  elrabf  2918  eueq2dc  2937  euxfrdc  2950  eqreu  2956  reu8  2960  ru  2988  sbcralt  3066  sbcrext  3067  sbcne12g  3102  csbnestgf  3137  dfss4st  3396  rexsng  3663  ralprg  3673  rexprg  3674  difsn  3759  opthpr  3802  ralunsn  3827  dfiin2g  3949  iunxsng  3992  iunxsngf  3994  elpwuni  4006  pwnss  4192  exmid01  4231  opelopabt  4296  opelopabga  4297  brabga  4298  opelopabgf  4304  elsucg  4439  elsuc2g  4440  brab2a  4716  opeliunxp  4718  posng  4735  brab2ga  4738  csbdmg  4860  elrnmpt1  4917  elrnmptg  4918  eliniseg2  5049  poleloe  5069  elxp4  5157  elxp5  5158  cnvpom  5212  sbcfung  5282  dffun8  5286  fncnv  5324  fununi  5326  fnssresb  5370  fnimaeq0  5379  funcocnv2  5529  dffn5im  5606  funimass4  5611  fnsnfv  5620  dmfco  5629  fndmdif  5667  fndmin  5669  unpreima  5687  respreima  5690  fsn2  5736  fnressn  5748  fressnfv  5749  elunirn  5813  dff13  5815  fliftel  5840  isoini  5865  f1oiso  5873  acexmid  5921  eloprabga  6009  resoprab2  6019  ralrnmpo  6037  rexrnmpo  6038  ovid  6039  ov  6042  ovg  6062  ofrfval2  6152  fmpox  6258  1stconst  6279  2ndconst  6280  f1od2  6293  rbropapd  6300  brtpos2  6309  dfsmo2  6345  frecabcl  6457  brdifun  6619  eqerlem  6623  brecop  6684  erovlem  6686  mapsn  6749  mptelixpg  6793  map1  6871  xpsnen  6880  xpdom2  6890  xpf1o  6905  supubti  7065  infglbti  7091  ctssdccl  7177  nninfwlpoim  7244  netap  7321  2omotaplemap  7324  ltpiord  7386  nlt1pig  7408  elinp  7541  ltdfpr  7573  genpassl  7591  genpassu  7592  1idprl  7657  1idpru  7658  gt0srpr  7815  mappsrprg  7871  map2psrprg  7872  peano2nnnn  7920  recidpirq  7925  axprecex  7947  xrlenlt  8091  addsubeq4  8241  renegcl  8287  lesub0  8506  recexaplem2  8679  conjmulap  8756  rerecclap  8757  creui  8987  peano2nn  9002  nndiv  9031  elznn0  9341  eqreznegel  9688  negelrp  9762  ltxr  9850  divelunit  10077  iccf1o  10079  elfz2  10090  elfzp1  10147  fzdifsuc  10156  fznn  10164  nelfzo  10227  fzosplitsni  10311  fvinim0ffz  10317  infssuzex  10323  zsupssdc  10328  frec2uzisod  10499  sq11i  10721  wrdval  10938  csbwrdg  10964  cjreb  11031  rexfiuz  11154  cau3lem  11279  pwm1geoserap1  11673  mertensabs  11702  divides  11954  dvdsabseq  12012  odd2np1  12038  oddm1even  12040  modremain  12094  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlema  12166  bezoutlemb  12167  isprm2  12285  isprm4  12287  dvdsnprmd  12293  oddprmdvds  12523  4sqlem2  12558  4sqlem12  12571  xpsfrnel2  12989  issubm  13104  grplmulf1o  13206  grplactcnv  13234  issubg  13303  elnmz  13338  isghm  13373  ghmeqker  13401  srg1zr  13543  iscrng2  13571  issubrng  13755  aprval  13838  zndvds  14205  znleval  14209  psrbag  14223  istopg  14235  basgen2  14317  isnei  14380  restdis  14420  iscn  14433  iscnp  14435  lmbr2  14450  lmbrf  14451  txcn  14511  cnmpt21  14527  blres  14670  isxms2  14688  metrest  14742  metcnp  14748  txmetcnp  14754  txmetcn  14755  cnblcld  14771  reopnap  14782  ioocosf1o  15090  mpodvdsmulf1o  15226  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  2lgslem1a  15329  bj-nn0sucALT  15624  apdiff  15692