Theorem bitrd 188

Description: Deduction form of bitri 184. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)

Hypotheses

Ref	Expression
bitrd.1	|- ( ph -> ( ps <-> ch ) )
bitrd.2	|- ( ph -> ( ch <-> th ) )

Assertion

Ref	Expression
bitrd	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitrd

Step	Hyp	Ref	Expression
1		bitrd.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2	1	pm5.74i 180	. . 3 |- ( ( ph -> ps ) <-> ( ph -> ch ) )
3		bitrd.2	. . . 4 |- ( ph -> ( ch <-> th ) )
4	3	pm5.74i 180	. . 3 |- ( ( ph -> ch ) <-> ( ph -> th ) )
5	2, 4	bitri 184	. 2 |- ( ( ph -> ps ) <-> ( ph -> th ) )
6	5	pm5.74ri 181	1 |- ( ph -> ( ps <-> 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:  bitr2d  189  bitr3d  190  bitr4d  191  bitrid  192  bitrdi  196  3bitrd  214  3bitr2d  216  3bitr3d  218  3bitr4d  220  imbi12d  234  bibi12d  235  sylan9bb  462  anbi12d  473  orbi12d  798  con1biidc  882  pm4.54dc  907  dn1dc  966  dedlem0a  974  dfifp3dc  988  dfifp4dc  989  dfifp5dc  990  3bior2fd  1388  xorbi12d  1424  nbbndc  1436  eleq12d  2300  neeq12d  2420  neleq12d  2501  raleqbi1dv  2740  rexeqbi1dv  2741  reueqd  2742  rmoeqd  2743  raleqbidv  2744  rexeqbidv  2745  raleqbidva  2746  rexeqbidva  2747  eueq3dc  2977  sbc19.21g  3097  sbcabel  3111  sbcel1g  3143  sbceq1g  3144  sbcel2g  3145  sbceq2g  3146  sbccsb2g  3154  sbcco3g  3182  sseq12d  3255  raaanlem  3596  sbcssg  3600  ralsng  3706  2ralunsn  3876  csbunig  3895  disjeq12d  4067  breq123d  4096  sbcbr12g  4138  sbcbr1g  4139  sbcbr2g  4140  treq  4187  nalset  4213  exmidsssn  4285  copsex4g  4332  onsucb  4594  posng  4790  csbxpg  4799  sbcrel  4804  csbcnvg  4905  eliniseg  5097  brcodir  5115  csbrng  5189  sbcfung  5341  fneq12d  5412  feq12d  5462  feq123d  5463  sbcfng  5470  sbcfg  5471  f1osng  5613  csbfv12g  5666  funimass4  5683  dmfco  5701  eqfnfv  5731  eqfnfv2  5732  fneqeql2  5743  fvimacnvi  5748  funimass3  5750  fniniseg  5754  rexsupp  5758  unpreima  5759  ralrnmpt  5776  rexrnmpt  5777  dffo3  5781  fmptco  5800  fressnfv  5825  eufnfv  5869  foima2  5874  fnunirn  5890  dff13  5891  f1elima  5896  cocan1  5910  cocan2  5911  fliftel  5916  fliftf  5922  isoresbr  5932  isoini  5941  f1oiso  5949  f1ofveu  5988  mpoeq123dva  6064  ovid  6120  ov  6123  ovg  6143  ovelrn  6153  caovord2d  6174  ofrfval2  6233  offveqb  6236  eqop  6321  reldm  6330  f1od2  6379  mpoxopoveq  6384  mpoxopovel  6385  tpostpos  6408  smoiso  6446  frecabcl  6543  frecsuclem  6550  nnaordr  6654  nnaword  6655  nnaordex  6672  ereq1  6685  brdifun  6705  erth2  6725  qliftfun  6762  brecop  6770  elmapg  6806  elpmg  6809  dom2lem  6921  xpcomco  6981  pw2f1odclem  6991  php5fin  7040  elfi2  7135  supisolem  7171  inflbti  7187  inl11  7228  ismkvnex  7318  mkvprop  7321  nninfwlporlemd  7335  exmidfodomrlemreseldju  7374  ltapig  7521  ltmpig  7522  nlt1pig  7524  mulcmpblnq  7551  ltsonq  7581  lt2addnq  7587  lt2mulnq  7588  archnqq  7600  prarloclemarch  7601  ltrnqg  7603  mulcmpblnq0  7627  preqlu  7655  genpdflem  7690  addnqprllem  7710  addnqprulem  7711  addlocprlemgt  7717  appdivnq  7746  mulnqprl  7751  mulnqpru  7752  mullocprlem  7753  distrlem4prl  7767  distrlem4pru  7768  1idprl  7773  1idpru  7774  ltexprlemloc  7790  cauappcvgprlemladdrl  7840  cauappcvgprlemladd  7841  cauappcvgprlem1  7842  archrecnq  7846  caucvgprlemnkj  7849  caucvgprprlemexb  7890  addcmpblnr  7922  lttrsr  7945  ltsosr  7947  ltasrg  7953  mulextsr1  7964  srpospr  7966  caucvgsrlemcau  7976  caucvgsrlemgt1  7978  caucvgsrlemoffres  7983  map2psrprg  7988  ltresr  8022  axcaucvglemres  8082  eqlelt  8229  cnegexlem1  8317  negeu  8333  subadd2  8346  subcan2  8367  addrsub  8513  ltaddneg  8567  ltaddnegr  8568  ltadd1  8572  leadd2  8574  ltsubadd  8575  lesubadd  8577  ltaddsub2  8580  leaddsub2  8582  ltaddpos  8595  lesub2  8600  ltsub2  8602  ltnegcon1  8606  ltnegcon2  8607  lenegcon1  8609  lenegcon2  8610  addge01  8615  addge02  8616  suble0  8619  leaddle0  8620  lesub0  8622  eqord2  8627  sublt0d  8713  recexre  8721  reaplt  8731  reapltxor  8732  reapneg  8740  remulext1  8742  apreim  8746  apcotr  8750  apadd2  8752  addext  8753  apsub1  8785  mulcanap2d  8805  diveqap0  8825  diveqap1  8848  apmul2  8932  ltmul2  8999  lemul2  9000  ltmulgt11  9007  ltmulgt12  9008  gt0div  9013  ge0div  9014  ltmuldiv  9017  ltrec1  9031  lerec2  9032  ledivdiv  9033  ltdiv23  9035  lediv23  9036  suprleubex  9097  creur  9102  creui  9103  nn1suc  9125  nnrecl  9363  znnsub  9494  zgt0ge1  9501  zltlen  9521  nn0n0n1ge2b  9522  nn0le2is012  9525  btwnnz  9537  gtndiv  9538  prime  9542  eluz2  9724  indstr2  9800  negm  9806  nn01to3  9808  qapne  9830  qltlen  9831  qreccl  9833  irrmulap  9839  divlt1lt  9916  divle1le  9917  nnledivrp  9958  xnn0xadd0  10059  xltadd2  10069  xsubge0  10073  xlesubadd  10075  iccid  10117  elioc2  10128  elico2  10129  elicc2  10130  elfz2  10207  fzen  10235  fzsubel  10252  elfzp1  10264  fzpr  10269  fzrevral2  10298  fzrevral3  10299  nn0disj  10330  2ffzeq  10333  fzosplitsni  10436  fvinim0ffz  10442  ioo0  10474  ico0  10476  ioc0  10477  modq0  10546  negqmod0  10548  zmodidfzo  10570  frecuzrdgtcl  10629  nn0ennn  10650  nninfinf  10660  sq11  10829  nn0le2msqd  10936  nn0opth2d  10940  hashen  11001  zfz1isolem1  11057  zfz1iso  11058  csbwrdg  11096  wrdnval  11097  eqwrd  11107  ccat0  11126  ccatws1lenp1bg  11163  swrd0g  11187  swrdspsleq  11194  pfxeq  11223  pfxsuffeqwrdeq  11225  pfxsuff1eqwrdeq  11226  ccatopth2  11244  wrd2ind  11250  2shfti  11337  cjap  11412  cnreim  11484  rexfiuz  11495  rexanuz2  11497  abs00ap  11568  absext  11569  sqabs  11588  abslt  11594  absle  11595  absdiflt  11598  absdifle  11599  lenegsq  11601  minmax  11736  ltmininf  11741  mingeb  11748  xrminmax  11771  xrmin1inf  11773  xrmin2inf  11774  xrltmininf  11776  xrlemininf  11777  clim  11787  clim0c  11792  climrecvg1n  11854  zsumdc  11890  fsum2dlemstep  11940  binomlem  11989  pwm1geoserap1  12014  zproddc  12085  efieq  12241  sin01bnd  12263  cos01bnd  12264  dvdsval2  12296  modm1div  12306  zdvdsdc  12318  modmulconst  12329  dvdsaddr  12343  dvdsabseq  12353  fzocongeq  12364  zeo3  12374  odd2np1  12379  oddp1d2  12396  zob  12397  oddm1d2  12398  nnoddm1d2  12416  divalgb  12431  divalgmod  12433  modremain  12435  bits0  12454  bitsp1e  12458  bitsp1o  12459  bitscmp  12464  bitsinv1lem  12467  gcdn0gt0  12494  bezoutlemstep  12513  dvdssq  12547  nn0seqcvgd  12558  algcvgblem  12566  lcmdvds  12596  lcmgcdeq  12600  coprmdvds  12609  qredeq  12613  congr  12617  isprm2  12634  isprm3  12635  prmdvdsexp  12665  prmdvdsexpb  12666  prmexpb  12668  prmfac1  12669  cncongrprm  12674  oddpwdclemxy  12686  oddpwdclemodd  12689  qnumdenbi  12709  qnumgt0  12715  hashdvds  12738  crth  12741  fermltl  12751  modprminveq  12768  pcpremul  12811  pc2dvds  12848  pcz  12850  prmpwdvds  12873  4sqlem16  12924  oddennn  12958  ctinfomlemom  12993  prdsbasmpt  13308  prdsbasmpt2  13316  mgm1  13398  ismhm  13489  mhmpropd  13494  issubm  13500  issubm2  13501  grpsubrcan  13609  grplactcnv  13630  grp1  13634  eqgval  13755  eqgid  13758  quselbasg  13762  isghm  13775  conjnmzb  13812  iscmn  13825  eqgabl  13862  rngmneg1  13905  rngmneg2  13906  rngpropd  13913  srgen1zr  13946  ringideu  13975  ringpropd  13996  crngpropd  13997  dvdsrd  14052  dvdsr02  14063  opprunitd  14068  crngunit  14069  unitpropdg  14106  rhmunitinv  14136  isnzr2  14142  issubrng  14157  resrhm2b  14207  aprval  14240  islmod  14249  islssm  14315  islssmg  14316  ellspsn  14375  isridl  14462  zrhrhmb  14580  zndvds  14607  znleval  14611  istopg  14667  eltg  14720  eltg2  14721  tgss2  14747  bastop1  14751  bastop2  14752  iscld  14771  isnei  14812  neiint  14813  iscn  14865  iscnp  14867  iscnp3  14871  tgcn  14876  ssidcn  14878  lmbr2  14882  lmbrf  14883  cnnei  14900  cnrest2  14904  eltx  14927  imasnopn  14967  ispsmet  14991  ismet  15012  isxmet  15013  metn0  15046  xmetres2  15047  elbl3ps  15062  elbl3  15063  xblpnfps  15066  xblpnf  15067  elmopn2  15117  metss  15162  bdxmet  15169  metrest  15174  xmetxp  15175  xmetxpbl  15176  metcnp3  15179  metcnp  15180  metcnp2  15181  metcn  15182  txmetcnp  15186  txmetcn  15187  metcnpd  15188  bl2ioo  15218  addcncntoplem  15229  elcncf  15241  elcncf2  15242  ivthdec  15312  ellimc3apf  15328  cnlimcim  15339  dveflem  15394  ply1termlem  15410  sincosq2sgn  15495  sinq12gt0  15498  logltb  15542  ltexp2  15609  wilthlem1  15648  lgsdilem  15700  lgsdir2lem4  15704  lgsdir2  15706  lgsne0  15711  lgsabs1  15712  gausslemma2dlem3  15736  gausslemma2dlem7  15741  lgseisenlem3  15745  lgsquad3  15757  2lgslem1a  15761  2lgslem3c  15768  2lgslem3d  15769  2lgsoddprmlem4  15785  2sqlem7  15794  2sqlem8a  15795  uhgreq12g  15870  isuhgropm  15875  uhgr0e  15876  upgrop  15898  uhgrvtxedgiedgb  15935  isuspgropen  15956  isusgropen  15957  uhgr2edg  15998  iswlk  16029  cbvrald  16110  bj-nalset  16216  bj-sels  16235  bj-nnelirr  16274  isomninnlem  16357  iswomninnlem  16376  iswomni0  16378  ismkvnnlem  16379