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  5614  csbfv12g  5667  funimass4  5684  dmfco  5702  eqfnfv  5732  eqfnfv2  5733  fneqeql2  5744  fvimacnvi  5749  funimass3  5751  fniniseg  5755  rexsupp  5759  unpreima  5760  ralrnmpt  5777  rexrnmpt  5778  dffo3  5782  fmptco  5801  fressnfv  5826  eufnfv  5870  foima2  5875  fnunirn  5891  dff13  5892  f1elima  5897  cocan1  5911  cocan2  5912  fliftel  5917  fliftf  5923  isoresbr  5933  isoini  5942  f1oiso  5950  f1ofveu  5989  mpoeq123dva  6065  ovid  6121  ov  6124  ovg  6144  ovelrn  6154  caovord2d  6175  ofrfval2  6235  offveqb  6238  eqop  6323  reldm  6332  f1od2  6381  mpoxopoveq  6386  mpoxopovel  6387  tpostpos  6410  smoiso  6448  frecabcl  6545  frecsuclem  6552  nnaordr  6656  nnaword  6657  nnaordex  6674  ereq1  6687  brdifun  6707  erth2  6727  qliftfun  6764  brecop  6772  elmapg  6808  elpmg  6811  dom2lem  6923  xpcomco  6985  pw2f1odclem  6995  php5fin  7044  elfi2  7139  supisolem  7175  inflbti  7191  inl11  7232  ismkvnex  7322  mkvprop  7325  nninfwlporlemd  7339  exmidfodomrlemreseldju  7378  ltapig  7525  ltmpig  7526  nlt1pig  7528  mulcmpblnq  7555  ltsonq  7585  lt2addnq  7591  lt2mulnq  7592  archnqq  7604  prarloclemarch  7605  ltrnqg  7607  mulcmpblnq0  7631  preqlu  7659  genpdflem  7694  addnqprllem  7714  addnqprulem  7715  addlocprlemgt  7721  appdivnq  7750  mulnqprl  7755  mulnqpru  7756  mullocprlem  7757  distrlem4prl  7771  distrlem4pru  7772  1idprl  7777  1idpru  7778  ltexprlemloc  7794  cauappcvgprlemladdrl  7844  cauappcvgprlemladd  7845  cauappcvgprlem1  7846  archrecnq  7850  caucvgprlemnkj  7853  caucvgprprlemexb  7894  addcmpblnr  7926  lttrsr  7949  ltsosr  7951  ltasrg  7957  mulextsr1  7968  srpospr  7970  caucvgsrlemcau  7980  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  map2psrprg  7992  ltresr  8026  axcaucvglemres  8086  eqlelt  8233  cnegexlem1  8321  negeu  8337  subadd2  8350  subcan2  8371  addrsub  8517  ltaddneg  8571  ltaddnegr  8572  ltadd1  8576  leadd2  8578  ltsubadd  8579  lesubadd  8581  ltaddsub2  8584  leaddsub2  8586  ltaddpos  8599  lesub2  8604  ltsub2  8606  ltnegcon1  8610  ltnegcon2  8611  lenegcon1  8613  lenegcon2  8614  addge01  8619  addge02  8620  suble0  8623  leaddle0  8624  lesub0  8626  eqord2  8631  sublt0d  8717  recexre  8725  reaplt  8735  reapltxor  8736  reapneg  8744  remulext1  8746  apreim  8750  apcotr  8754  apadd2  8756  addext  8757  apsub1  8789  mulcanap2d  8809  diveqap0  8829  diveqap1  8852  apmul2  8936  ltmul2  9003  lemul2  9004  ltmulgt11  9011  ltmulgt12  9012  gt0div  9017  ge0div  9018  ltmuldiv  9021  ltrec1  9035  lerec2  9036  ledivdiv  9037  ltdiv23  9039  lediv23  9040  suprleubex  9101  creur  9106  creui  9107  nn1suc  9129  nnrecl  9367  znnsub  9498  zgt0ge1  9505  zltlen  9525  nn0n0n1ge2b  9526  nn0le2is012  9529  btwnnz  9541  gtndiv  9542  prime  9546  eluz2  9728  indstr2  9804  negm  9810  nn01to3  9812  qapne  9834  qltlen  9835  qreccl  9837  irrmulap  9843  divlt1lt  9920  divle1le  9921  nnledivrp  9962  xnn0xadd0  10063  xltadd2  10073  xsubge0  10077  xlesubadd  10079  iccid  10121  elioc2  10132  elico2  10133  elicc2  10134  elfz2  10211  fzen  10239  fzsubel  10256  elfzp1  10268  fzpr  10273  fzrevral2  10302  fzrevral3  10303  nn0disj  10334  2ffzeq  10337  fzosplitsni  10441  fvinim0ffz  10447  ioo0  10479  ico0  10481  ioc0  10482  modq0  10551  negqmod0  10553  zmodidfzo  10575  frecuzrdgtcl  10634  nn0ennn  10655  nninfinf  10665  sq11  10834  nn0le2msqd  10941  nn0opth2d  10945  hashen  11006  zfz1isolem1  11062  zfz1iso  11063  csbwrdg  11101  wrdnval  11102  eqwrd  11112  ccat0  11131  ccatws1lenp1bg  11168  swrd0g  11192  swrdspsleq  11199  pfxeq  11228  pfxsuffeqwrdeq  11230  pfxsuff1eqwrdeq  11231  ccatopth2  11249  wrd2ind  11255  2shfti  11342  cjap  11417  cnreim  11489  rexfiuz  11500  rexanuz2  11502  abs00ap  11573  absext  11574  sqabs  11593  abslt  11599  absle  11600  absdiflt  11603  absdifle  11604  lenegsq  11606  minmax  11741  ltmininf  11746  mingeb  11753  xrminmax  11776  xrmin1inf  11778  xrmin2inf  11779  xrltmininf  11781  xrlemininf  11782  clim  11792  clim0c  11797  climrecvg1n  11859  zsumdc  11895  fsum2dlemstep  11945  binomlem  11994  pwm1geoserap1  12019  zproddc  12090  efieq  12246  sin01bnd  12268  cos01bnd  12269  dvdsval2  12301  modm1div  12311  zdvdsdc  12323  modmulconst  12334  dvdsaddr  12348  dvdsabseq  12358  fzocongeq  12369  zeo3  12379  odd2np1  12384  oddp1d2  12401  zob  12402  oddm1d2  12403  nnoddm1d2  12421  divalgb  12436  divalgmod  12438  modremain  12440  bits0  12459  bitsp1e  12463  bitsp1o  12464  bitscmp  12469  bitsinv1lem  12472  gcdn0gt0  12499  bezoutlemstep  12518  dvdssq  12552  nn0seqcvgd  12563  algcvgblem  12571  lcmdvds  12601  lcmgcdeq  12605  coprmdvds  12614  qredeq  12618  congr  12622  isprm2  12639  isprm3  12640  prmdvdsexp  12670  prmdvdsexpb  12671  prmexpb  12673  prmfac1  12674  cncongrprm  12679  oddpwdclemxy  12691  oddpwdclemodd  12694  qnumdenbi  12714  qnumgt0  12720  hashdvds  12743  crth  12746  fermltl  12756  modprminveq  12773  pcpremul  12816  pc2dvds  12853  pcz  12855  prmpwdvds  12878  4sqlem16  12929  oddennn  12963  ctinfomlemom  12998  prdsbasmpt  13313  prdsbasmpt2  13321  mgm1  13403  ismhm  13494  mhmpropd  13499  issubm  13505  issubm2  13506  grpsubrcan  13614  grplactcnv  13635  grp1  13639  eqgval  13760  eqgid  13763  quselbasg  13767  isghm  13780  conjnmzb  13817  iscmn  13830  eqgabl  13867  rngmneg1  13910  rngmneg2  13911  rngpropd  13918  srgen1zr  13951  ringideu  13980  ringpropd  14001  crngpropd  14002  dvdsrd  14058  dvdsr02  14069  opprunitd  14074  crngunit  14075  unitpropdg  14112  rhmunitinv  14142  isnzr2  14148  issubrng  14163  resrhm2b  14213  aprval  14246  islmod  14255  islssm  14321  islssmg  14322  ellspsn  14381  isridl  14468  zrhrhmb  14586  zndvds  14613  znleval  14617  istopg  14673  eltg  14726  eltg2  14727  tgss2  14753  bastop1  14757  bastop2  14758  iscld  14777  isnei  14818  neiint  14819  iscn  14871  iscnp  14873  iscnp3  14877  tgcn  14882  ssidcn  14884  lmbr2  14888  lmbrf  14889  cnnei  14906  cnrest2  14910  eltx  14933  imasnopn  14973  ispsmet  14997  ismet  15018  isxmet  15019  metn0  15052  xmetres2  15053  elbl3ps  15068  elbl3  15069  xblpnfps  15072  xblpnf  15073  elmopn2  15123  metss  15168  bdxmet  15175  metrest  15180  xmetxp  15181  xmetxpbl  15182  metcnp3  15185  metcnp  15186  metcnp2  15187  metcn  15188  txmetcnp  15192  txmetcn  15193  metcnpd  15194  bl2ioo  15224  addcncntoplem  15235  elcncf  15247  elcncf2  15248  ivthdec  15318  ellimc3apf  15334  cnlimcim  15345  dveflem  15400  ply1termlem  15416  sincosq2sgn  15501  sinq12gt0  15504  logltb  15548  ltexp2  15615  wilthlem1  15654  lgsdilem  15706  lgsdir2lem4  15710  lgsdir2  15712  lgsne0  15717  lgsabs1  15718  gausslemma2dlem3  15742  gausslemma2dlem7  15747  lgseisenlem3  15751  lgsquad3  15763  2lgslem1a  15767  2lgslem3c  15774  2lgslem3d  15775  2lgsoddprmlem4  15791  2sqlem7  15800  2sqlem8a  15801  uhgreq12g  15876  isuhgropm  15881  uhgr0e  15882  upgrop  15904  uhgrvtxedgiedgb  15941  isuspgropen  15962  isusgropen  15963  uhgr2edg  16004  iswlk  16036  upgriswlkdc  16071  cbvrald  16152  bj-nalset  16258  bj-sels  16277  bj-nnelirr  16316  isomninnlem  16398  iswomninnlem  16417  iswomni0  16419  ismkvnnlem  16420