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  800  con1biidc  884  pm4.54dc  909  dn1dc  968  dedlem0a  976  dfifp3dc  990  dfifp4dc  991  dfifp5dc  992  3bior2fd  1390  xorbi12d  1426  nbbndc  1438  eleq12d  2302  neeq12d  2422  neleq12d  2503  raleqbi1dv  2742  rexeqbi1dv  2743  reueqd  2744  rmoeqd  2745  raleqbidv  2746  rexeqbidv  2747  raleqbidva  2748  rexeqbidva  2749  eueq3dc  2980  sbc19.21g  3100  sbcabel  3114  sbcel1g  3146  sbceq1g  3147  sbcel2g  3148  sbceq2g  3149  sbccsb2g  3157  sbcco3g  3185  sseq12d  3258  raaanlem  3599  sbcssg  3603  ralsng  3709  2ralunsn  3882  csbunig  3901  disjeq12d  4073  breq123d  4102  sbcbr12g  4144  sbcbr1g  4145  sbcbr2g  4146  treq  4193  nalset  4219  exmidsssn  4292  copsex4g  4339  onsucb  4601  posng  4798  csbxpg  4807  sbcrel  4812  csbcnvg  4914  eliniseg  5106  brcodir  5124  csbrng  5198  sbcfung  5350  fneq12d  5422  feq12d  5472  feq123d  5473  sbcfng  5480  sbcfg  5481  f1osng  5626  csbfv12g  5679  funimass4  5696  dmfco  5714  eqfnfv  5744  eqfnfv2  5745  fneqeql2  5756  fvimacnvi  5761  funimass3  5763  fniniseg  5767  rexsupp  5771  unpreima  5772  ralrnmpt  5789  rexrnmpt  5790  dffo3  5794  fmptco  5813  fressnfv  5841  eufnfv  5885  foima2  5892  fnunirn  5908  dff13  5909  f1elima  5914  cocan1  5928  cocan2  5929  fliftel  5934  fliftf  5940  isoresbr  5950  isoini  5959  f1oiso  5967  f1ofveu  6006  mpoeq123dva  6082  ovid  6138  ov  6141  ovg  6161  ovelrn  6171  caovord2d  6192  ofrfval2  6252  offveqb  6255  eqop  6340  reldm  6349  f1od2  6400  mpoxopoveq  6406  mpoxopovel  6407  tpostpos  6430  smoiso  6468  frecabcl  6565  frecsuclem  6572  nnaordr  6678  nnaword  6679  nnaordex  6696  ereq1  6709  brdifun  6729  erth2  6749  qliftfun  6786  brecop  6794  elmapg  6830  elpmg  6833  dom2lem  6945  xpcomco  7010  pw2f1odclem  7020  php5fin  7071  elfi2  7171  supisolem  7207  inflbti  7223  inl11  7264  ismkvnex  7354  mkvprop  7357  nninfwlporlemd  7371  exmidfodomrlemreseldju  7411  ltapig  7558  ltmpig  7559  nlt1pig  7561  mulcmpblnq  7588  ltsonq  7618  lt2addnq  7624  lt2mulnq  7625  archnqq  7637  prarloclemarch  7638  ltrnqg  7640  mulcmpblnq0  7664  preqlu  7692  genpdflem  7727  addnqprllem  7747  addnqprulem  7748  addlocprlemgt  7754  appdivnq  7783  mulnqprl  7788  mulnqpru  7789  mullocprlem  7790  distrlem4prl  7804  distrlem4pru  7805  1idprl  7810  1idpru  7811  ltexprlemloc  7827  cauappcvgprlemladdrl  7877  cauappcvgprlemladd  7878  cauappcvgprlem1  7879  archrecnq  7883  caucvgprlemnkj  7886  caucvgprprlemexb  7927  addcmpblnr  7959  lttrsr  7982  ltsosr  7984  ltasrg  7990  mulextsr1  8001  srpospr  8003  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  map2psrprg  8025  ltresr  8059  axcaucvglemres  8119  eqlelt  8266  cnegexlem1  8354  negeu  8370  subadd2  8383  subcan2  8404  addrsub  8550  ltaddneg  8604  ltaddnegr  8605  ltadd1  8609  leadd2  8611  ltsubadd  8612  lesubadd  8614  ltaddsub2  8617  leaddsub2  8619  ltaddpos  8632  lesub2  8637  ltsub2  8639  ltnegcon1  8643  ltnegcon2  8644  lenegcon1  8646  lenegcon2  8647  addge01  8652  addge02  8653  suble0  8656  leaddle0  8657  lesub0  8659  eqord2  8664  sublt0d  8750  recexre  8758  reaplt  8768  reapltxor  8769  reapneg  8777  remulext1  8779  apreim  8783  apcotr  8787  apadd2  8789  addext  8790  apsub1  8822  mulcanap2d  8842  diveqap0  8862  diveqap1  8885  apmul2  8969  ltmul2  9036  lemul2  9037  ltmulgt11  9044  ltmulgt12  9045  gt0div  9050  ge0div  9051  ltmuldiv  9054  ltrec1  9068  lerec2  9069  ledivdiv  9070  ltdiv23  9072  lediv23  9073  suprleubex  9134  creur  9139  creui  9140  nn1suc  9162  nnrecl  9400  znnsub  9531  zgt0ge1  9538  zltlen  9558  nn0n0n1ge2b  9559  nn0le2is012  9562  btwnnz  9574  gtndiv  9575  prime  9579  eluz2  9761  indstr2  9843  negm  9849  nn01to3  9851  qapne  9873  qltlen  9874  qreccl  9876  irrmulap  9882  divlt1lt  9959  divle1le  9960  nnledivrp  10001  xnn0xadd0  10102  xltadd2  10112  xsubge0  10116  xlesubadd  10118  iccid  10160  elioc2  10171  elico2  10172  elicc2  10173  elfz2  10250  fzen  10278  fzsubel  10295  elfzp1  10307  fzpr  10312  fzrevral2  10341  fzrevral3  10342  nn0disj  10373  2ffzeq  10376  fzosplitsni  10482  fvinim0ffz  10488  ioo0  10520  ico0  10522  ioc0  10523  modq0  10592  negqmod0  10594  zmodidfzo  10616  frecuzrdgtcl  10675  nn0ennn  10696  nninfinf  10706  sq11  10875  nn0le2msqd  10982  nn0opth2d  10986  hashen  11047  zfz1isolem1  11105  zfz1iso  11106  csbwrdg  11147  wrdnval  11148  eqwrd  11158  ccat0  11177  ccatws1lenp1bg  11216  swrd0g  11245  swrdspsleq  11252  pfxeq  11281  pfxsuffeqwrdeq  11283  pfxsuff1eqwrdeq  11284  ccatopth2  11302  wrd2ind  11308  2shfti  11396  cjap  11471  cnreim  11543  rexfiuz  11554  rexanuz2  11556  abs00ap  11627  absext  11628  sqabs  11647  abslt  11653  absle  11654  absdiflt  11657  absdifle  11658  lenegsq  11660  minmax  11795  ltmininf  11800  mingeb  11807  xrminmax  11830  xrmin1inf  11832  xrmin2inf  11833  xrltmininf  11835  xrlemininf  11836  clim  11846  clim0c  11851  climrecvg1n  11913  zsumdc  11950  fsum2dlemstep  12000  binomlem  12049  pwm1geoserap1  12074  zproddc  12145  efieq  12301  sin01bnd  12323  cos01bnd  12324  dvdsval2  12356  modm1div  12366  zdvdsdc  12378  modmulconst  12389  dvdsaddr  12403  dvdsabseq  12413  fzocongeq  12424  zeo3  12434  odd2np1  12439  oddp1d2  12456  zob  12457  oddm1d2  12458  nnoddm1d2  12476  divalgb  12491  divalgmod  12493  modremain  12495  bits0  12514  bitsp1e  12518  bitsp1o  12519  bitscmp  12524  bitsinv1lem  12527  gcdn0gt0  12554  bezoutlemstep  12573  dvdssq  12607  nn0seqcvgd  12618  algcvgblem  12626  lcmdvds  12656  lcmgcdeq  12660  coprmdvds  12669  qredeq  12673  congr  12677  isprm2  12694  isprm3  12695  prmdvdsexp  12725  prmdvdsexpb  12726  prmexpb  12728  prmfac1  12729  cncongrprm  12734  oddpwdclemxy  12746  oddpwdclemodd  12749  qnumdenbi  12769  qnumgt0  12775  hashdvds  12798  crth  12801  fermltl  12811  modprminveq  12828  pcpremul  12871  pc2dvds  12908  pcz  12910  prmpwdvds  12933  4sqlem16  12984  oddennn  13018  ctinfomlemom  13053  prdsbasmpt  13368  prdsbasmpt2  13376  mgm1  13458  ismhm  13549  mhmpropd  13554  issubm  13560  issubm2  13561  grpsubrcan  13669  grplactcnv  13690  grp1  13694  eqgval  13815  eqgid  13818  quselbasg  13822  isghm  13835  conjnmzb  13872  iscmn  13885  eqgabl  13922  rngmneg1  13966  rngmneg2  13967  rngpropd  13974  srgen1zr  14007  ringideu  14036  ringpropd  14057  crngpropd  14058  dvdsrd  14114  dvdsr02  14125  opprunitd  14130  crngunit  14131  unitpropdg  14168  rhmunitinv  14198  isnzr2  14204  issubrng  14219  resrhm2b  14269  aprval  14302  islmod  14311  islssm  14377  islssmg  14378  ellspsn  14437  isridl  14524  zrhrhmb  14642  zndvds  14669  znleval  14673  istopg  14729  eltg  14782  eltg2  14783  tgss2  14809  bastop1  14813  bastop2  14814  iscld  14833  isnei  14874  neiint  14875  iscn  14927  iscnp  14929  iscnp3  14933  tgcn  14938  ssidcn  14940  lmbr2  14944  lmbrf  14945  cnnei  14962  cnrest2  14966  eltx  14989  imasnopn  15029  ispsmet  15053  ismet  15074  isxmet  15075  metn0  15108  xmetres2  15109  elbl3ps  15124  elbl3  15125  xblpnfps  15128  xblpnf  15129  elmopn2  15179  metss  15224  bdxmet  15231  metrest  15236  xmetxp  15237  xmetxpbl  15238  metcnp3  15241  metcnp  15242  metcnp2  15243  metcn  15244  txmetcnp  15248  txmetcn  15249  metcnpd  15250  bl2ioo  15280  addcncntoplem  15291  elcncf  15303  elcncf2  15304  ivthdec  15374  ellimc3apf  15390  cnlimcim  15401  dveflem  15456  ply1termlem  15472  sincosq2sgn  15557  sinq12gt0  15560  logltb  15604  ltexp2  15671  wilthlem1  15710  lgsdilem  15762  lgsdir2lem4  15766  lgsdir2  15768  lgsne0  15773  lgsabs1  15774  gausslemma2dlem3  15798  gausslemma2dlem7  15803  lgseisenlem3  15807  lgsquad3  15819  2lgslem1a  15823  2lgslem3c  15830  2lgslem3d  15831  2lgsoddprmlem4  15847  2sqlem7  15856  2sqlem8a  15857  uhgreq12g  15933  isuhgropm  15938  uhgr0e  15939  upgrop  15961  uhgrvtxedgiedgb  16000  isuspgropen  16021  isusgropen  16022  uhgr2edg  16063  issubgr2  16115  uhgrspansubgrlem  16133  vtxd0nedgbfi  16156  1loopgrvd0fi  16163  iswlk  16180  upgriswlkdc  16217  istrl  16242  iseupth  16304  eupth2lem2dc  16316  eupth2lem3lem3fi  16327  eupth2lem3lem4fi  16330  eupth2lem3lem7fi  16331  cbvrald  16410  bj-nalset  16516  bj-sels  16535  bj-nnelirr  16574  isomninnlem  16660  iswomninnlem  16680  iswomni0  16682  ismkvnnlem  16683