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  4296  exmid01  4335  opelopabt  4404  opelopabga  4405  brabga  4406  opelopabgf  4412  elsucg  4549  elsuc2g  4550  brab2a  4828  opeliunxp  4830  posng  4847  brab2ga  4850  csbdmg  4975  elrnmpt1  5033  elrnmptg  5034  eliniseg2  5167  poleloe  5187  elxp4  5275  elxp5  5276  cnvpom  5330  sbcfung  5401  dffun8  5405  fncnv  5447  fununi  5449  fnssresb  5495  fnimaeq0  5505  funcocnv2  5664  dffn5im  5748  funimass4  5753  fnsnfv  5762  dmfco  5773  fndmdif  5814  fndmin  5816  unpreima  5833  respreima  5836  fsn2  5882  fnressn  5901  fressnfv  5902  elunirn  5972  dff13  5974  fliftel  5999  isoini  6024  f1oiso  6032  riotaeqimp  6063  acexmid  6084  fnbrovb  6130  eloprabga  6175  resoprab2  6185  ralrnmpo  6203  rexrnmpo  6204  ovid  6205  ov  6208  ovg  6228  ofrfval2  6319  fmpox  6436  1stconst  6457  2ndconst  6458  f1od2  6471  rbropapd  6513  brtpos2  6522  dfsmo2  6558  frecabcl  6670  brdifun  6834  eqerlem  6838  brecop  6899  erovlem  6901  mapfset  6945  mapsnd  6970  mapsn  6972  mptelixpg  7016  map1  7101  xpsnen  7119  xpdom2  7129  xpf1o  7144  mapunen  7151  supubti  7339  infglbti  7365  ctssdccl  7451  nninfwlpoim  7519  nninfinfwlpo  7520  netap  7620  2omotaplemap  7623  ltpiord  7686  nlt1pig  7708  elinp  7841  ltdfpr  7873  genpassl  7891  genpassu  7892  1idprl  7957  1idpru  7958  gt0srpr  8115  mappsrprg  8171  map2psrprg  8172  peano2nnnn  8220  recidpirq  8225  axprecex  8247  xrlenlt  8390  addsubeq4  8542  renegcl  8588  lesub0  8808  recexaplem2  8982  conjmulap  9061  rerecclap  9062  creui  9292  peano2nn  9318  nndiv  9347  elznn0  9663  eqreznegel  10023  negelrp  10098  ltxr  10187  divelunit  10414  iccf1o  10417  elfz2  10428  elfzp1  10489  fzdifsuc  10498  fznn  10506  nelfzo  10569  fzosplitsni  10664  fvinim0ffz  10670  infssuzex  10676  zsupssdc  10683  frec2uzisod  10857  sq11i  11079  nn0sqdc  11160  wrdval  11321  csbwrdg  11348  swrdnd  11445  wrd2ind  11509  cjreb  11645  rexfiuz  11769  cau3lem  11895  pwm1geoserap1  12291  mertensabs  12320  divides  12572  dvdsabseq  12630  odd2np1  12656  oddm1even  12658  modremain  12712  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlema  12792  bezoutlemb  12793  isprm2  12911  isprm4  12913  dvdsnprmd  12919  nnmaxpw  12969  oddprmdvds  13153  4sqlem2  13188  4sqlem12  13201  xpsfrnel2  13716  issubm  13828  grplmulf1o  13928  grplactcnv  13956  issubg  14025  elnmz  14060  isghm  14095  ghmeqker  14123  rng1zrlem  14307  iscrng2  14368  issubrng  14556  aprval  14640  zndvds  15033  znleval  15037  psrbag  15102  istopg  15149  basgen2  15231  isnei  15294  restdis  15334  iscn  15347  iscnp  15349  lmbr2  15364  lmbrf  15365  txcn  15425  cnmpt21  15441  blres  15584  isxms2  15602  metrest  15656  metcnp  15662  txmetcnp  15668  txmetcn  15669  cnblcld  15685  reopnap  15696  ioocosf1o  16005  mpodvdsmulf1o  16185  gausslemma2dlem0i  16274  gausslemma2dlem1a  16275  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  2lgslem1a  16305  isuhgrm  16410  isushgrm  16411  isupgren  16434  isumgren  16444  isuspgren  16496  isusgren  16497  uhgr0v0e  16573  vtxdg0v  16633  iswlk  16662  wlk1walkdom  16698  istrl  16724  clwwlkn1  16757  clwwlkn2  16760  clwwlknonel  16771  clwwlknun  16780  iseupth  16786  eupthres  16796  eupth2lem1  16797  eupth2lemsfi  16817  bj-nn0sucALT  17102  apdiff  17195  ralrals  17247  rexrals  17248  ralals  17253  rexals  17254