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  2978  sbc19.21g  3098  sbcabel  3112  sbcel1g  3144  sbceq1g  3145  sbcel2g  3146  sbceq2g  3147  sbccsb2g  3155  sbcco3g  3183  sseq12d  3256  raaanlem  3597  sbcssg  3601  ralsng  3707  2ralunsn  3880  csbunig  3899  disjeq12d  4071  breq123d  4100  sbcbr12g  4142  sbcbr1g  4143  sbcbr2g  4144  treq  4191  nalset  4217  exmidsssn  4290  copsex4g  4337  onsucb  4599  posng  4796  csbxpg  4805  sbcrel  4810  csbcnvg  4912  eliniseg  5104  brcodir  5122  csbrng  5196  sbcfung  5348  fneq12d  5419  feq12d  5469  feq123d  5470  sbcfng  5477  sbcfg  5478  f1osng  5622  csbfv12g  5675  funimass4  5692  dmfco  5710  eqfnfv  5740  eqfnfv2  5741  fneqeql2  5752  fvimacnvi  5757  funimass3  5759  fniniseg  5763  rexsupp  5767  unpreima  5768  ralrnmpt  5785  rexrnmpt  5786  dffo3  5790  fmptco  5809  fressnfv  5836  eufnfv  5880  foima2  5887  fnunirn  5903  dff13  5904  f1elima  5909  cocan1  5923  cocan2  5924  fliftel  5929  fliftf  5935  isoresbr  5945  isoini  5954  f1oiso  5962  f1ofveu  6001  mpoeq123dva  6077  ovid  6133  ov  6136  ovg  6156  ovelrn  6166  caovord2d  6187  ofrfval2  6247  offveqb  6250  eqop  6335  reldm  6344  f1od2  6395  mpoxopoveq  6401  mpoxopovel  6402  tpostpos  6425  smoiso  6463  frecabcl  6560  frecsuclem  6567  nnaordr  6673  nnaword  6674  nnaordex  6691  ereq1  6704  brdifun  6724  erth2  6744  qliftfun  6781  brecop  6789  elmapg  6825  elpmg  6828  dom2lem  6940  xpcomco  7005  pw2f1odclem  7015  php5fin  7064  elfi2  7162  supisolem  7198  inflbti  7214  inl11  7255  ismkvnex  7345  mkvprop  7348  nninfwlporlemd  7362  exmidfodomrlemreseldju  7401  ltapig  7548  ltmpig  7549  nlt1pig  7551  mulcmpblnq  7578  ltsonq  7608  lt2addnq  7614  lt2mulnq  7615  archnqq  7627  prarloclemarch  7628  ltrnqg  7630  mulcmpblnq0  7654  preqlu  7682  genpdflem  7717  addnqprllem  7737  addnqprulem  7738  addlocprlemgt  7744  appdivnq  7773  mulnqprl  7778  mulnqpru  7779  mullocprlem  7780  distrlem4prl  7794  distrlem4pru  7795  1idprl  7800  1idpru  7801  ltexprlemloc  7817  cauappcvgprlemladdrl  7867  cauappcvgprlemladd  7868  cauappcvgprlem1  7869  archrecnq  7873  caucvgprlemnkj  7876  caucvgprprlemexb  7917  addcmpblnr  7949  lttrsr  7972  ltsosr  7974  ltasrg  7980  mulextsr1  7991  srpospr  7993  caucvgsrlemcau  8003  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  map2psrprg  8015  ltresr  8049  axcaucvglemres  8109  eqlelt  8256  cnegexlem1  8344  negeu  8360  subadd2  8373  subcan2  8394  addrsub  8540  ltaddneg  8594  ltaddnegr  8595  ltadd1  8599  leadd2  8601  ltsubadd  8602  lesubadd  8604  ltaddsub2  8607  leaddsub2  8609  ltaddpos  8622  lesub2  8627  ltsub2  8629  ltnegcon1  8633  ltnegcon2  8634  lenegcon1  8636  lenegcon2  8637  addge01  8642  addge02  8643  suble0  8646  leaddle0  8647  lesub0  8649  eqord2  8654  sublt0d  8740  recexre  8748  reaplt  8758  reapltxor  8759  reapneg  8767  remulext1  8769  apreim  8773  apcotr  8777  apadd2  8779  addext  8780  apsub1  8812  mulcanap2d  8832  diveqap0  8852  diveqap1  8875  apmul2  8959  ltmul2  9026  lemul2  9027  ltmulgt11  9034  ltmulgt12  9035  gt0div  9040  ge0div  9041  ltmuldiv  9044  ltrec1  9058  lerec2  9059  ledivdiv  9060  ltdiv23  9062  lediv23  9063  suprleubex  9124  creur  9129  creui  9130  nn1suc  9152  nnrecl  9390  znnsub  9521  zgt0ge1  9528  zltlen  9548  nn0n0n1ge2b  9549  nn0le2is012  9552  btwnnz  9564  gtndiv  9565  prime  9569  eluz2  9751  indstr2  9833  negm  9839  nn01to3  9841  qapne  9863  qltlen  9864  qreccl  9866  irrmulap  9872  divlt1lt  9949  divle1le  9950  nnledivrp  9991  xnn0xadd0  10092  xltadd2  10102  xsubge0  10106  xlesubadd  10108  iccid  10150  elioc2  10161  elico2  10162  elicc2  10163  elfz2  10240  fzen  10268  fzsubel  10285  elfzp1  10297  fzpr  10302  fzrevral2  10331  fzrevral3  10332  nn0disj  10363  2ffzeq  10366  fzosplitsni  10471  fvinim0ffz  10477  ioo0  10509  ico0  10511  ioc0  10512  modq0  10581  negqmod0  10583  zmodidfzo  10605  frecuzrdgtcl  10664  nn0ennn  10685  nninfinf  10695  sq11  10864  nn0le2msqd  10971  nn0opth2d  10975  hashen  11036  zfz1isolem1  11094  zfz1iso  11095  csbwrdg  11133  wrdnval  11134  eqwrd  11144  ccat0  11163  ccatws1lenp1bg  11202  swrd0g  11231  swrdspsleq  11238  pfxeq  11267  pfxsuffeqwrdeq  11269  pfxsuff1eqwrdeq  11270  ccatopth2  11288  wrd2ind  11294  2shfti  11382  cjap  11457  cnreim  11529  rexfiuz  11540  rexanuz2  11542  abs00ap  11613  absext  11614  sqabs  11633  abslt  11639  absle  11640  absdiflt  11643  absdifle  11644  lenegsq  11646  minmax  11781  ltmininf  11786  mingeb  11793  xrminmax  11816  xrmin1inf  11818  xrmin2inf  11819  xrltmininf  11821  xrlemininf  11822  clim  11832  clim0c  11837  climrecvg1n  11899  zsumdc  11935  fsum2dlemstep  11985  binomlem  12034  pwm1geoserap1  12059  zproddc  12130  efieq  12286  sin01bnd  12308  cos01bnd  12309  dvdsval2  12341  modm1div  12351  zdvdsdc  12363  modmulconst  12374  dvdsaddr  12388  dvdsabseq  12398  fzocongeq  12409  zeo3  12419  odd2np1  12424  oddp1d2  12441  zob  12442  oddm1d2  12443  nnoddm1d2  12461  divalgb  12476  divalgmod  12478  modremain  12480  bits0  12499  bitsp1e  12503  bitsp1o  12504  bitscmp  12509  bitsinv1lem  12512  gcdn0gt0  12539  bezoutlemstep  12558  dvdssq  12592  nn0seqcvgd  12603  algcvgblem  12611  lcmdvds  12641  lcmgcdeq  12645  coprmdvds  12654  qredeq  12658  congr  12662  isprm2  12679  isprm3  12680  prmdvdsexp  12710  prmdvdsexpb  12711  prmexpb  12713  prmfac1  12714  cncongrprm  12719  oddpwdclemxy  12731  oddpwdclemodd  12734  qnumdenbi  12754  qnumgt0  12760  hashdvds  12783  crth  12786  fermltl  12796  modprminveq  12813  pcpremul  12856  pc2dvds  12893  pcz  12895  prmpwdvds  12918  4sqlem16  12969  oddennn  13003  ctinfomlemom  13038  prdsbasmpt  13353  prdsbasmpt2  13361  mgm1  13443  ismhm  13534  mhmpropd  13539  issubm  13545  issubm2  13546  grpsubrcan  13654  grplactcnv  13675  grp1  13679  eqgval  13800  eqgid  13803  quselbasg  13807  isghm  13820  conjnmzb  13857  iscmn  13870  eqgabl  13907  rngmneg1  13950  rngmneg2  13951  rngpropd  13958  srgen1zr  13991  ringideu  14020  ringpropd  14041  crngpropd  14042  dvdsrd  14098  dvdsr02  14109  opprunitd  14114  crngunit  14115  unitpropdg  14152  rhmunitinv  14182  isnzr2  14188  issubrng  14203  resrhm2b  14253  aprval  14286  islmod  14295  islssm  14361  islssmg  14362  ellspsn  14421  isridl  14508  zrhrhmb  14626  zndvds  14653  znleval  14657  istopg  14713  eltg  14766  eltg2  14767  tgss2  14793  bastop1  14797  bastop2  14798  iscld  14817  isnei  14858  neiint  14859  iscn  14911  iscnp  14913  iscnp3  14917  tgcn  14922  ssidcn  14924  lmbr2  14928  lmbrf  14929  cnnei  14946  cnrest2  14950  eltx  14973  imasnopn  15013  ispsmet  15037  ismet  15058  isxmet  15059  metn0  15092  xmetres2  15093  elbl3ps  15108  elbl3  15109  xblpnfps  15112  xblpnf  15113  elmopn2  15163  metss  15208  bdxmet  15215  metrest  15220  xmetxp  15221  xmetxpbl  15222  metcnp3  15225  metcnp  15226  metcnp2  15227  metcn  15228  txmetcnp  15232  txmetcn  15233  metcnpd  15234  bl2ioo  15264  addcncntoplem  15275  elcncf  15287  elcncf2  15288  ivthdec  15358  ellimc3apf  15374  cnlimcim  15385  dveflem  15440  ply1termlem  15456  sincosq2sgn  15541  sinq12gt0  15544  logltb  15588  ltexp2  15655  wilthlem1  15694  lgsdilem  15746  lgsdir2lem4  15750  lgsdir2  15752  lgsne0  15757  lgsabs1  15758  gausslemma2dlem3  15782  gausslemma2dlem7  15787  lgseisenlem3  15791  lgsquad3  15803  2lgslem1a  15807  2lgslem3c  15814  2lgslem3d  15815  2lgsoddprmlem4  15831  2sqlem7  15840  2sqlem8a  15841  uhgreq12g  15917  isuhgropm  15922  uhgr0e  15923  upgrop  15945  uhgrvtxedgiedgb  15982  isuspgropen  16003  isusgropen  16004  uhgr2edg  16045  vtxd0nedgbfi  16105  1loopgrvd0fi  16112  iswlk  16120  upgriswlkdc  16157  istrl  16180  iseupth  16242  cbvrald  16320  bj-nalset  16426  bj-sels  16445  bj-nnelirr  16484  isomninnlem  16570  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592