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  3877  csbunig  3896  disjeq12d  4068  breq123d  4097  sbcbr12g  4139  sbcbr1g  4140  sbcbr2g  4141  treq  4188  nalset  4214  exmidsssn  4286  copsex4g  4333  onsucb  4595  posng  4791  csbxpg  4800  sbcrel  4805  csbcnvg  4906  eliniseg  5098  brcodir  5116  csbrng  5190  sbcfung  5342  fneq12d  5413  feq12d  5463  feq123d  5464  sbcfng  5471  sbcfg  5472  f1osng  5616  csbfv12g  5669  funimass4  5686  dmfco  5704  eqfnfv  5734  eqfnfv2  5735  fneqeql2  5746  fvimacnvi  5751  funimass3  5753  fniniseg  5757  rexsupp  5761  unpreima  5762  ralrnmpt  5779  rexrnmpt  5780  dffo3  5784  fmptco  5803  fressnfv  5830  eufnfv  5874  foima2  5881  fnunirn  5897  dff13  5898  f1elima  5903  cocan1  5917  cocan2  5918  fliftel  5923  fliftf  5929  isoresbr  5939  isoini  5948  f1oiso  5956  f1ofveu  5995  mpoeq123dva  6071  ovid  6127  ov  6130  ovg  6150  ovelrn  6160  caovord2d  6181  ofrfval2  6241  offveqb  6244  eqop  6329  reldm  6338  f1od2  6387  mpoxopoveq  6392  mpoxopovel  6393  tpostpos  6416  smoiso  6454  frecabcl  6551  frecsuclem  6558  nnaordr  6664  nnaword  6665  nnaordex  6682  ereq1  6695  brdifun  6715  erth2  6735  qliftfun  6772  brecop  6780  elmapg  6816  elpmg  6819  dom2lem  6931  xpcomco  6993  pw2f1odclem  7003  php5fin  7052  elfi2  7150  supisolem  7186  inflbti  7202  inl11  7243  ismkvnex  7333  mkvprop  7336  nninfwlporlemd  7350  exmidfodomrlemreseldju  7389  ltapig  7536  ltmpig  7537  nlt1pig  7539  mulcmpblnq  7566  ltsonq  7596  lt2addnq  7602  lt2mulnq  7603  archnqq  7615  prarloclemarch  7616  ltrnqg  7618  mulcmpblnq0  7642  preqlu  7670  genpdflem  7705  addnqprllem  7725  addnqprulem  7726  addlocprlemgt  7732  appdivnq  7761  mulnqprl  7766  mulnqpru  7767  mullocprlem  7768  distrlem4prl  7782  distrlem4pru  7783  1idprl  7788  1idpru  7789  ltexprlemloc  7805  cauappcvgprlemladdrl  7855  cauappcvgprlemladd  7856  cauappcvgprlem1  7857  archrecnq  7861  caucvgprlemnkj  7864  caucvgprprlemexb  7905  addcmpblnr  7937  lttrsr  7960  ltsosr  7962  ltasrg  7968  mulextsr1  7979  srpospr  7981  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  map2psrprg  8003  ltresr  8037  axcaucvglemres  8097  eqlelt  8244  cnegexlem1  8332  negeu  8348  subadd2  8361  subcan2  8382  addrsub  8528  ltaddneg  8582  ltaddnegr  8583  ltadd1  8587  leadd2  8589  ltsubadd  8590  lesubadd  8592  ltaddsub2  8595  leaddsub2  8597  ltaddpos  8610  lesub2  8615  ltsub2  8617  ltnegcon1  8621  ltnegcon2  8622  lenegcon1  8624  lenegcon2  8625  addge01  8630  addge02  8631  suble0  8634  leaddle0  8635  lesub0  8637  eqord2  8642  sublt0d  8728  recexre  8736  reaplt  8746  reapltxor  8747  reapneg  8755  remulext1  8757  apreim  8761  apcotr  8765  apadd2  8767  addext  8768  apsub1  8800  mulcanap2d  8820  diveqap0  8840  diveqap1  8863  apmul2  8947  ltmul2  9014  lemul2  9015  ltmulgt11  9022  ltmulgt12  9023  gt0div  9028  ge0div  9029  ltmuldiv  9032  ltrec1  9046  lerec2  9047  ledivdiv  9048  ltdiv23  9050  lediv23  9051  suprleubex  9112  creur  9117  creui  9118  nn1suc  9140  nnrecl  9378  znnsub  9509  zgt0ge1  9516  zltlen  9536  nn0n0n1ge2b  9537  nn0le2is012  9540  btwnnz  9552  gtndiv  9553  prime  9557  eluz2  9739  indstr2  9816  negm  9822  nn01to3  9824  qapne  9846  qltlen  9847  qreccl  9849  irrmulap  9855  divlt1lt  9932  divle1le  9933  nnledivrp  9974  xnn0xadd0  10075  xltadd2  10085  xsubge0  10089  xlesubadd  10091  iccid  10133  elioc2  10144  elico2  10145  elicc2  10146  elfz2  10223  fzen  10251  fzsubel  10268  elfzp1  10280  fzpr  10285  fzrevral2  10314  fzrevral3  10315  nn0disj  10346  2ffzeq  10349  fzosplitsni  10453  fvinim0ffz  10459  ioo0  10491  ico0  10493  ioc0  10494  modq0  10563  negqmod0  10565  zmodidfzo  10587  frecuzrdgtcl  10646  nn0ennn  10667  nninfinf  10677  sq11  10846  nn0le2msqd  10953  nn0opth2d  10957  hashen  11018  zfz1isolem1  11075  zfz1iso  11076  csbwrdg  11114  wrdnval  11115  eqwrd  11125  ccat0  11144  ccatws1lenp1bg  11183  swrd0g  11207  swrdspsleq  11214  pfxeq  11243  pfxsuffeqwrdeq  11245  pfxsuff1eqwrdeq  11246  ccatopth2  11264  wrd2ind  11270  2shfti  11357  cjap  11432  cnreim  11504  rexfiuz  11515  rexanuz2  11517  abs00ap  11588  absext  11589  sqabs  11608  abslt  11614  absle  11615  absdiflt  11618  absdifle  11619  lenegsq  11621  minmax  11756  ltmininf  11761  mingeb  11768  xrminmax  11791  xrmin1inf  11793  xrmin2inf  11794  xrltmininf  11796  xrlemininf  11797  clim  11807  clim0c  11812  climrecvg1n  11874  zsumdc  11910  fsum2dlemstep  11960  binomlem  12009  pwm1geoserap1  12034  zproddc  12105  efieq  12261  sin01bnd  12283  cos01bnd  12284  dvdsval2  12316  modm1div  12326  zdvdsdc  12338  modmulconst  12349  dvdsaddr  12363  dvdsabseq  12373  fzocongeq  12384  zeo3  12394  odd2np1  12399  oddp1d2  12416  zob  12417  oddm1d2  12418  nnoddm1d2  12436  divalgb  12451  divalgmod  12453  modremain  12455  bits0  12474  bitsp1e  12478  bitsp1o  12479  bitscmp  12484  bitsinv1lem  12487  gcdn0gt0  12514  bezoutlemstep  12533  dvdssq  12567  nn0seqcvgd  12578  algcvgblem  12586  lcmdvds  12616  lcmgcdeq  12620  coprmdvds  12629  qredeq  12633  congr  12637  isprm2  12654  isprm3  12655  prmdvdsexp  12685  prmdvdsexpb  12686  prmexpb  12688  prmfac1  12689  cncongrprm  12694  oddpwdclemxy  12706  oddpwdclemodd  12709  qnumdenbi  12729  qnumgt0  12735  hashdvds  12758  crth  12761  fermltl  12771  modprminveq  12788  pcpremul  12831  pc2dvds  12868  pcz  12870  prmpwdvds  12893  4sqlem16  12944  oddennn  12978  ctinfomlemom  13013  prdsbasmpt  13328  prdsbasmpt2  13336  mgm1  13418  ismhm  13509  mhmpropd  13514  issubm  13520  issubm2  13521  grpsubrcan  13629  grplactcnv  13650  grp1  13654  eqgval  13775  eqgid  13778  quselbasg  13782  isghm  13795  conjnmzb  13832  iscmn  13845  eqgabl  13882  rngmneg1  13925  rngmneg2  13926  rngpropd  13933  srgen1zr  13966  ringideu  13995  ringpropd  14016  crngpropd  14017  dvdsrd  14073  dvdsr02  14084  opprunitd  14089  crngunit  14090  unitpropdg  14127  rhmunitinv  14157  isnzr2  14163  issubrng  14178  resrhm2b  14228  aprval  14261  islmod  14270  islssm  14336  islssmg  14337  ellspsn  14396  isridl  14483  zrhrhmb  14601  zndvds  14628  znleval  14632  istopg  14688  eltg  14741  eltg2  14742  tgss2  14768  bastop1  14772  bastop2  14773  iscld  14792  isnei  14833  neiint  14834  iscn  14886  iscnp  14888  iscnp3  14892  tgcn  14897  ssidcn  14899  lmbr2  14903  lmbrf  14904  cnnei  14921  cnrest2  14925  eltx  14948  imasnopn  14988  ispsmet  15012  ismet  15033  isxmet  15034  metn0  15067  xmetres2  15068  elbl3ps  15083  elbl3  15084  xblpnfps  15087  xblpnf  15088  elmopn2  15138  metss  15183  bdxmet  15190  metrest  15195  xmetxp  15196  xmetxpbl  15197  metcnp3  15200  metcnp  15201  metcnp2  15202  metcn  15203  txmetcnp  15207  txmetcn  15208  metcnpd  15209  bl2ioo  15239  addcncntoplem  15250  elcncf  15262  elcncf2  15263  ivthdec  15333  ellimc3apf  15349  cnlimcim  15360  dveflem  15415  ply1termlem  15431  sincosq2sgn  15516  sinq12gt0  15519  logltb  15563  ltexp2  15630  wilthlem1  15669  lgsdilem  15721  lgsdir2lem4  15725  lgsdir2  15727  lgsne0  15732  lgsabs1  15733  gausslemma2dlem3  15757  gausslemma2dlem7  15762  lgseisenlem3  15766  lgsquad3  15778  2lgslem1a  15782  2lgslem3c  15789  2lgslem3d  15790  2lgsoddprmlem4  15806  2sqlem7  15815  2sqlem8a  15816  uhgreq12g  15891  isuhgropm  15896  uhgr0e  15897  upgrop  15919  uhgrvtxedgiedgb  15956  isuspgropen  15977  isusgropen  15978  uhgr2edg  16019  iswlk  16064  upgriswlkdc  16101  istrl  16124  cbvrald  16207  bj-nalset  16313  bj-sels  16332  bj-nnelirr  16371  isomninnlem  16458  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480