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  801  con1biidc  885  pm4.54dc  910  dn1dc  969  dedlem0a  977  dfifp3dc  991  dfifp4dc  992  dfifp5dc  993  3bior2fd  1391  xorbi12d  1427  nbbndc  1439  eleq12d  2302  neeq12d  2423  neleq12d  2504  raleqbi1dv  2743  rexeqbi1dv  2744  reueqd  2745  rmoeqd  2746  raleqbidv  2747  rexeqbidv  2748  raleqbidva  2749  rexeqbidva  2750  eueq3dc  2981  sbc19.21g  3101  sbcabel  3115  sbcel1g  3147  sbceq1g  3148  sbcel2g  3149  sbceq2g  3150  sbccsb2g  3158  sbcco3g  3186  sseq12d  3259  raaanlem  3601  sbcssg  3605  ralsng  3713  2ralunsn  3887  csbunig  3906  disjeq12d  4078  breq123d  4107  sbcbr12g  4149  sbcbr1g  4150  sbcbr2g  4151  treq  4198  nalset  4224  exmidsssn  4298  copsex4g  4345  onsucb  4607  posng  4804  csbxpg  4813  sbcrel  4818  csbcnvg  4920  eliniseg  5113  brcodir  5131  csbrng  5205  sbcfung  5357  fneq12d  5429  feq12d  5479  feq123d  5480  sbcfng  5487  sbcfg  5488  f1osng  5635  csbfv12g  5688  funimass4  5705  dmfco  5723  eqfnfv  5753  eqfnfv2  5754  fneqeql2  5765  fvimacnvi  5770  funimass3  5772  fniniseg  5776  unpreima  5780  ralrnmpt  5797  rexrnmpt  5798  dffo3  5802  fmptco  5821  fressnfv  5849  eufnfv  5895  foima2  5902  fnunirn  5918  dff13  5919  f1elima  5924  cocan1  5938  cocan2  5939  fliftel  5944  fliftf  5950  isoresbr  5960  isoini  5969  f1oiso  5977  f1ofveu  6016  mpoeq123dva  6092  ovid  6148  ov  6151  ovg  6171  ovelrn  6181  caovord2d  6202  ofrfval2  6261  offveqb  6264  eqop  6349  reldm  6358  f1od2  6409  suppval1  6417  suppssrst  6439  suppssrgst  6440  mpoxopoveq  6449  mpoxopovel  6450  tpostpos  6473  smoiso  6511  frecabcl  6608  frecsuclem  6615  nnaordr  6721  nnaword  6722  nnaordex  6739  ereq1  6752  brdifun  6772  erth2  6792  qliftfun  6829  brecop  6837  elmapg  6873  elpmg  6876  dom2lem  6988  xpcomco  7053  pw2f1odclem  7063  php5fin  7114  elfi2  7214  supisolem  7250  inflbti  7266  inl11  7307  ismkvnex  7397  mkvprop  7400  nninfwlporlemd  7414  exmidfodomrlemreseldju  7454  ltapig  7601  ltmpig  7602  nlt1pig  7604  mulcmpblnq  7631  ltsonq  7661  lt2addnq  7667  lt2mulnq  7668  archnqq  7680  prarloclemarch  7681  ltrnqg  7683  mulcmpblnq0  7707  preqlu  7735  genpdflem  7770  addnqprllem  7790  addnqprulem  7791  addlocprlemgt  7797  appdivnq  7826  mulnqprl  7831  mulnqpru  7832  mullocprlem  7833  distrlem4prl  7847  distrlem4pru  7848  1idprl  7853  1idpru  7854  ltexprlemloc  7870  cauappcvgprlemladdrl  7920  cauappcvgprlemladd  7921  cauappcvgprlem1  7922  archrecnq  7926  caucvgprlemnkj  7929  caucvgprprlemexb  7970  addcmpblnr  8002  lttrsr  8025  ltsosr  8027  ltasrg  8033  mulextsr1  8044  srpospr  8046  caucvgsrlemcau  8056  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  map2psrprg  8068  ltresr  8102  axcaucvglemres  8162  eqlelt  8308  cnegexlem1  8396  negeu  8412  subadd2  8425  subcan2  8446  addrsub  8592  ltaddneg  8646  ltaddnegr  8647  ltadd1  8651  leadd2  8653  ltsubadd  8654  lesubadd  8656  ltaddsub2  8659  leaddsub2  8661  ltaddpos  8674  lesub2  8679  ltsub2  8681  ltnegcon1  8685  ltnegcon2  8686  lenegcon1  8688  lenegcon2  8689  addge01  8694  addge02  8695  suble0  8698  leaddle0  8699  lesub0  8701  eqord2  8706  sublt0d  8792  recexre  8800  reaplt  8810  reapltxor  8811  reapneg  8819  remulext1  8821  apreim  8825  apcotr  8829  apadd2  8831  addext  8832  apsub1  8864  mulcanap2d  8884  diveqap0  8904  diveqap1  8927  apmul2  9011  ltmul2  9078  lemul2  9079  ltmulgt11  9086  ltmulgt12  9087  gt0div  9092  ge0div  9093  ltmuldiv  9096  ltrec1  9110  lerec2  9111  ledivdiv  9112  ltdiv23  9114  lediv23  9115  suprleubex  9176  creur  9181  creui  9182  nn1suc  9204  nnrecl  9442  znnsub  9575  zgt0ge1  9582  zltlen  9602  nn0n0n1ge2b  9603  nn0le2is012  9606  btwnnz  9618  gtndiv  9619  prime  9623  eluz2  9805  indstr2  9887  negm  9893  nn01to3  9895  qapne  9917  qltlen  9918  qreccl  9920  irrmulap  9926  divlt1lt  10003  divle1le  10004  nnledivrp  10045  xnn0xadd0  10146  xltadd2  10156  xsubge0  10160  xlesubadd  10162  iccid  10204  elioc2  10215  elico2  10216  elicc2  10217  elfz2  10295  fzen  10323  fzsubel  10340  elfzp1  10352  fzpr  10357  fzrevral2  10386  fzrevral3  10387  nn0disj  10418  2ffzeq  10421  fzosplitsni  10527  fvinim0ffz  10533  ioo0  10565  ico0  10567  ioc0  10568  modq0  10637  negqmod0  10639  zmodidfzo  10661  frecuzrdgtcl  10720  nn0ennn  10741  nninfinf  10751  sq11  10920  nn0le2msqd  11027  nn0opth2d  11031  hashen  11092  zfz1isolem1  11150  zfz1iso  11151  csbwrdg  11192  wrdnval  11193  eqwrd  11203  ccat0  11222  ccatws1lenp1bg  11261  swrd0g  11290  swrdspsleq  11297  pfxeq  11326  pfxsuffeqwrdeq  11328  pfxsuff1eqwrdeq  11329  ccatopth2  11347  wrd2ind  11353  2shfti  11454  cjap  11529  cnreim  11601  rexfiuz  11612  rexanuz2  11614  abs00ap  11685  absext  11686  sqabs  11705  abslt  11711  absle  11712  absdiflt  11715  absdifle  11716  lenegsq  11718  minmax  11853  ltmininf  11858  mingeb  11865  xrminmax  11888  xrmin1inf  11890  xrmin2inf  11891  xrltmininf  11893  xrlemininf  11894  clim  11904  clim0c  11909  climrecvg1n  11971  zsumdc  12008  fsum2dlemstep  12058  binomlem  12107  pwm1geoserap1  12132  zproddc  12203  efieq  12359  sin01bnd  12381  cos01bnd  12382  dvdsval2  12414  modm1div  12424  zdvdsdc  12436  modmulconst  12447  dvdsaddr  12461  dvdsabseq  12471  fzocongeq  12482  zeo3  12492  odd2np1  12497  oddp1d2  12514  zob  12515  oddm1d2  12516  nnoddm1d2  12534  divalgb  12549  divalgmod  12551  modremain  12553  bits0  12572  bitsp1e  12576  bitsp1o  12577  bitscmp  12582  bitsinv1lem  12585  gcdn0gt0  12612  bezoutlemstep  12631  dvdssq  12665  nn0seqcvgd  12676  algcvgblem  12684  lcmdvds  12714  lcmgcdeq  12718  coprmdvds  12727  qredeq  12731  congr  12735  isprm2  12752  isprm3  12753  prmdvdsexp  12783  prmdvdsexpb  12784  prmexpb  12786  prmfac1  12787  cncongrprm  12792  oddpwdclemxy  12804  oddpwdclemodd  12807  qnumdenbi  12827  qnumgt0  12833  hashdvds  12856  crth  12859  fermltl  12869  modprminveq  12886  pcpremul  12929  pc2dvds  12966  pcz  12968  prmpwdvds  12991  4sqlem16  13042  oddennn  13076  ctinfomlemom  13111  prdsbasmpt  13426  prdsbasmpt2  13434  mgm1  13516  ismhm  13607  mhmpropd  13612  issubm  13618  issubm2  13619  grpsubrcan  13727  grplactcnv  13748  grp1  13752  eqgval  13873  eqgid  13876  quselbasg  13880  isghm  13893  conjnmzb  13930  iscmn  13943  eqgabl  13980  rngmneg1  14024  rngmneg2  14025  rngpropd  14032  srgen1zr  14065  ringideu  14094  ringpropd  14115  crngpropd  14116  dvdsrd  14172  dvdsr02  14183  opprunitd  14188  crngunit  14189  unitpropdg  14226  rhmunitinv  14256  isnzr2  14262  issubrng  14277  resrhm2b  14327  aprval  14361  islmod  14370  islssm  14436  islssmg  14437  ellspsn  14496  isridl  14583  zrhrhmb  14701  zndvds  14728  znleval  14732  istopg  14793  eltg  14846  eltg2  14847  tgss2  14873  bastop1  14877  bastop2  14878  iscld  14897  isnei  14938  neiint  14939  iscn  14991  iscnp  14993  iscnp3  14997  tgcn  15002  ssidcn  15004  lmbr2  15008  lmbrf  15009  cnnei  15026  cnrest2  15030  eltx  15053  imasnopn  15093  ispsmet  15117  ismet  15138  isxmet  15139  metn0  15172  xmetres2  15173  elbl3ps  15188  elbl3  15189  xblpnfps  15192  xblpnf  15193  elmopn2  15243  metss  15288  bdxmet  15295  metrest  15300  xmetxp  15301  xmetxpbl  15302  metcnp3  15305  metcnp  15306  metcnp2  15307  metcn  15308  txmetcnp  15312  txmetcn  15313  metcnpd  15314  bl2ioo  15344  addcncntoplem  15355  elcncf  15367  elcncf2  15368  ivthdec  15438  ellimc3apf  15454  cnlimcim  15465  dveflem  15520  ply1termlem  15536  sincosq2sgn  15621  sinq12gt0  15624  logltb  15668  ltexp2  15735  wilthlem1  15777  lgsdilem  15829  lgsdir2lem4  15833  lgsdir2  15835  lgsne0  15840  lgsabs1  15841  gausslemma2dlem3  15865  gausslemma2dlem7  15870  lgseisenlem3  15874  lgsquad3  15886  2lgslem1a  15890  2lgslem3c  15897  2lgslem3d  15898  2lgsoddprmlem4  15914  2sqlem7  15923  2sqlem8a  15924  uhgreq12g  16000  isuhgropm  16005  uhgr0e  16006  upgrop  16028  uhgrvtxedgiedgb  16067  isuspgropen  16088  isusgropen  16089  uhgr2edg  16130  issubgr2  16182  uhgrspansubgrlem  16200  vtxd0nedgbfi  16223  1loopgrvd0fi  16230  iswlk  16247  upgriswlkdc  16284  istrl  16309  iseupth  16371  eupth2lem2dc  16383  eupth2lem3lem3fi  16394  eupth2lem3lem4fi  16397  eupth2lem3lem7fi  16398  cbvrald  16489  bj-nalset  16594  bj-sels  16613  bj-nnelirr  16652  isomninnlem  16745  iswomninnlem  16765  iswomni0  16767  ismkvnnlem  16768