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  suppinisegdc  6513  rbropapd  6518  brtpos2  6527  dfsmo2  6563  frecabcl  6675  brdifun  6839  eqerlem  6843  brecop  6904  erovlem  6906  mapfset  6950  mapsnd  6976  mapsn  6978  mptelixpg  7022  map1  7107  xpsnen  7125  xpdom2  7135  xpf1o  7150  mapunen  7157  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  9668  eqreznegel  10029  negelrp  10104  ltxr  10193  divelunit  10420  iccf1o  10423  elfz2  10434  elfzp1  10495  fzdifsuc  10504  fznn  10512  nelfzo  10575  fzosplitsni  10670  fvinim0ffz  10676  infssuzex  10682  zsupssdc  10689  frec2uzisod  10864  sq11i  11086  nn0sqdc  11167  wrdval  11328  csbwrdg  11355  swrdnd  11452  wrd2ind  11516  cjreb  11652  rexfiuz  11776  cau3lem  11902  pwm1geoserap1  12299  mertensabs  12328  divides  12580  dvdsabseq  12638  odd2np1  12664  oddm1even  12666  modremain  12720  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlema  12800  bezoutlemb  12801  isprm2  12919  isprm4  12921  dvdsnprmd  12927  nnmaxpw  12977  oddprmdvds  13161  4sqlem2  13196  4sqlem12  13209  xpsfrnel2  13725  issubm  13837  grplmulf1o  13937  grplactcnv  13965  issubg  14034  elnmz  14069  isghm  14104  ghmeqker  14132  resscntz  14165  cntzsgrpcl  14166  rng1zrlem  14364  iscrng2  14425  issubrng  14615  aprval  14699  zndvds  15092  znleval  15096  psrbag  15163  istopg  15242  basgen2  15324  isnei  15387  restdis  15427  iscn  15440  iscnp  15442  lmbr2  15457  lmbrf  15458  txcn  15518  cnmpt21  15534  blres  15677  isxms2  15695  metrest  15749  metcnp  15755  txmetcnp  15761  txmetcn  15762  cnblcld  15778  reopnap  15789  sineq0re  16093  ioocosf1o  16099  mpodvdsmulf1o  16301  gausslemma2dlem0i  16398  gausslemma2dlem1a  16399  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  2lgslem1a  16429  isuhgrm  16534  isushgrm  16535  isupgren  16558  isumgren  16568  isuspgren  16620  isusgren  16621  uhgr0v0e  16697  vtxdg0v  16757  iswlk  16786  wlk1walkdom  16822  istrl  16848  clwwlkn1  16881  clwwlkn2  16884  clwwlknonel  16895  clwwlknun  16904  iseupth  16910  eupthres  16920  eupth2lem1  16921  eupth2lemsfi  16941  bj-nn0sucALT  17226  apdiff  17321  ralrals  17373  rexrals  17374  ralals  17379  rexals  17380