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  795  con1biidc  879  pm4.54dc  904  dn1dc  963  dedlem0a  971  3bior2fd  1366  xorbi12d  1402  nbbndc  1414  eleq12d  2277  neeq12d  2397  neleq12d  2478  raleqbi1dv  2715  rexeqbi1dv  2716  reueqd  2717  rmoeqd  2718  raleqbidv  2719  rexeqbidv  2720  raleqbidva  2721  rexeqbidva  2722  eueq3dc  2951  sbc19.21g  3071  sbcabel  3084  sbcel1g  3116  sbceq1g  3117  sbcel2g  3118  sbceq2g  3119  sbccsb2g  3127  sbcco3g  3155  sseq12d  3228  raaanlem  3569  sbcssg  3573  ralsng  3678  2ralunsn  3848  csbunig  3867  disjeq12d  4039  breq123d  4068  sbcbr12g  4110  sbcbr1g  4111  sbcbr2g  4112  treq  4159  nalset  4185  exmidsssn  4257  copsex4g  4304  onsucb  4564  posng  4760  csbxpg  4769  sbcrel  4774  csbcnvg  4875  eliniseg  5066  brcodir  5084  csbrng  5158  sbcfung  5309  fneq12d  5380  feq12d  5430  feq123d  5431  sbcfng  5438  sbcfg  5439  f1osng  5581  csbfv12g  5632  funimass4  5647  dmfco  5665  eqfnfv  5695  eqfnfv2  5696  fneqeql2  5707  fvimacnvi  5712  funimass3  5714  fniniseg  5718  rexsupp  5722  unpreima  5723  ralrnmpt  5740  rexrnmpt  5741  dffo3  5745  fmptco  5764  fressnfv  5789  eufnfv  5833  foima2  5838  fnunirn  5854  dff13  5855  f1elima  5860  cocan1  5874  cocan2  5875  fliftel  5880  fliftf  5886  isoresbr  5896  isoini  5905  f1oiso  5913  f1ofveu  5950  mpoeq123dva  6024  ovid  6080  ov  6083  ovg  6103  ovelrn  6113  caovord2d  6134  ofrfval2  6193  offveqb  6196  eqop  6281  reldm  6290  f1od2  6339  mpoxopoveq  6344  mpoxopovel  6345  tpostpos  6368  smoiso  6406  frecabcl  6503  frecsuclem  6510  nnaordr  6614  nnaword  6615  nnaordex  6632  ereq1  6645  brdifun  6665  erth2  6685  qliftfun  6722  brecop  6730  elmapg  6766  elpmg  6769  dom2lem  6881  xpcomco  6941  pw2f1odclem  6951  php5fin  7000  elfi2  7095  supisolem  7131  inflbti  7147  inl11  7188  ismkvnex  7278  mkvprop  7281  nninfwlporlemd  7295  exmidfodomrlemreseldju  7334  ltapig  7481  ltmpig  7482  nlt1pig  7484  mulcmpblnq  7511  ltsonq  7541  lt2addnq  7547  lt2mulnq  7548  archnqq  7560  prarloclemarch  7561  ltrnqg  7563  mulcmpblnq0  7587  preqlu  7615  genpdflem  7650  addnqprllem  7670  addnqprulem  7671  addlocprlemgt  7677  appdivnq  7706  mulnqprl  7711  mulnqpru  7712  mullocprlem  7713  distrlem4prl  7727  distrlem4pru  7728  1idprl  7733  1idpru  7734  ltexprlemloc  7750  cauappcvgprlemladdrl  7800  cauappcvgprlemladd  7801  cauappcvgprlem1  7802  archrecnq  7806  caucvgprlemnkj  7809  caucvgprprlemexb  7850  addcmpblnr  7882  lttrsr  7905  ltsosr  7907  ltasrg  7913  mulextsr1  7924  srpospr  7926  caucvgsrlemcau  7936  caucvgsrlemgt1  7938  caucvgsrlemoffres  7943  map2psrprg  7948  ltresr  7982  axcaucvglemres  8042  eqlelt  8189  cnegexlem1  8277  negeu  8293  subadd2  8306  subcan2  8327  addrsub  8473  ltaddneg  8527  ltaddnegr  8528  ltadd1  8532  leadd2  8534  ltsubadd  8535  lesubadd  8537  ltaddsub2  8540  leaddsub2  8542  ltaddpos  8555  lesub2  8560  ltsub2  8562  ltnegcon1  8566  ltnegcon2  8567  lenegcon1  8569  lenegcon2  8570  addge01  8575  addge02  8576  suble0  8579  leaddle0  8580  lesub0  8582  eqord2  8587  sublt0d  8673  recexre  8681  reaplt  8691  reapltxor  8692  reapneg  8700  remulext1  8702  apreim  8706  apcotr  8710  apadd2  8712  addext  8713  apsub1  8745  mulcanap2d  8765  diveqap0  8785  diveqap1  8808  apmul2  8892  ltmul2  8959  lemul2  8960  ltmulgt11  8967  ltmulgt12  8968  gt0div  8973  ge0div  8974  ltmuldiv  8977  ltrec1  8991  lerec2  8992  ledivdiv  8993  ltdiv23  8995  lediv23  8996  suprleubex  9057  creur  9062  creui  9063  nn1suc  9085  nnrecl  9323  znnsub  9454  zgt0ge1  9461  zltlen  9481  nn0n0n1ge2b  9482  nn0le2is012  9485  btwnnz  9497  gtndiv  9498  prime  9502  eluz2  9684  indstr2  9760  negm  9766  nn01to3  9768  qapne  9790  qltlen  9791  qreccl  9793  irrmulap  9799  divlt1lt  9876  divle1le  9877  nnledivrp  9918  xnn0xadd0  10019  xltadd2  10029  xsubge0  10033  xlesubadd  10035  iccid  10077  elioc2  10088  elico2  10089  elicc2  10090  elfz2  10167  fzen  10195  fzsubel  10212  elfzp1  10224  fzpr  10229  fzrevral2  10258  fzrevral3  10259  nn0disj  10290  2ffzeq  10293  fzosplitsni  10396  fvinim0ffz  10402  ioo0  10434  ico0  10436  ioc0  10437  modq0  10506  negqmod0  10508  zmodidfzo  10530  frecuzrdgtcl  10589  nn0ennn  10610  nninfinf  10620  sq11  10789  nn0le2msqd  10896  nn0opth2d  10900  hashen  10961  zfz1isolem1  11017  zfz1iso  11018  csbwrdg  11055  wrdnval  11056  eqwrd  11066  ccat0  11085  ccatws1lenp1bg  11122  swrd0g  11146  swrdspsleq  11153  pfxeq  11182  pfxsuffeqwrdeq  11184  pfxsuff1eqwrdeq  11185  ccatopth2  11203  wrd2ind  11209  2shfti  11227  cjap  11302  cnreim  11374  rexfiuz  11385  rexanuz2  11387  abs00ap  11458  absext  11459  sqabs  11478  abslt  11484  absle  11485  absdiflt  11488  absdifle  11489  lenegsq  11491  minmax  11626  ltmininf  11631  mingeb  11638  xrminmax  11661  xrmin1inf  11663  xrmin2inf  11664  xrltmininf  11666  xrlemininf  11667  clim  11677  clim0c  11682  climrecvg1n  11744  zsumdc  11780  fsum2dlemstep  11830  binomlem  11879  pwm1geoserap1  11904  zproddc  11975  efieq  12131  sin01bnd  12153  cos01bnd  12154  dvdsval2  12186  modm1div  12196  zdvdsdc  12208  modmulconst  12219  dvdsaddr  12233  dvdsabseq  12243  fzocongeq  12254  zeo3  12264  odd2np1  12269  oddp1d2  12286  zob  12287  oddm1d2  12288  nnoddm1d2  12306  divalgb  12321  divalgmod  12323  modremain  12325  bits0  12344  bitsp1e  12348  bitsp1o  12349  bitscmp  12354  bitsinv1lem  12357  gcdn0gt0  12384  bezoutlemstep  12403  dvdssq  12437  nn0seqcvgd  12448  algcvgblem  12456  lcmdvds  12486  lcmgcdeq  12490  coprmdvds  12499  qredeq  12503  congr  12507  isprm2  12524  isprm3  12525  prmdvdsexp  12555  prmdvdsexpb  12556  prmexpb  12558  prmfac1  12559  cncongrprm  12564  oddpwdclemxy  12576  oddpwdclemodd  12579  qnumdenbi  12599  qnumgt0  12605  hashdvds  12628  crth  12631  fermltl  12641  modprminveq  12658  pcpremul  12701  pc2dvds  12738  pcz  12740  prmpwdvds  12763  4sqlem16  12814  oddennn  12848  ctinfomlemom  12883  prdsbasmpt  13197  prdsbasmpt2  13205  mgm1  13287  ismhm  13378  mhmpropd  13383  issubm  13389  issubm2  13390  grpsubrcan  13498  grplactcnv  13519  grp1  13523  eqgval  13644  eqgid  13647  quselbasg  13651  isghm  13664  conjnmzb  13701  iscmn  13714  eqgabl  13751  rngmneg1  13794  rngmneg2  13795  rngpropd  13802  srgen1zr  13835  ringideu  13864  ringpropd  13885  crngpropd  13886  dvdsrd  13941  dvdsr02  13952  opprunitd  13957  crngunit  13958  unitpropdg  13995  rhmunitinv  14025  isnzr2  14031  issubrng  14046  resrhm2b  14096  aprval  14129  islmod  14138  islssm  14204  islssmg  14205  ellspsn  14264  isridl  14351  zrhrhmb  14469  zndvds  14496  znleval  14500  istopg  14556  eltg  14609  eltg2  14610  tgss2  14636  bastop1  14640  bastop2  14641  iscld  14660  isnei  14701  neiint  14702  iscn  14754  iscnp  14756  iscnp3  14760  tgcn  14765  ssidcn  14767  lmbr2  14771  lmbrf  14772  cnnei  14789  cnrest2  14793  eltx  14816  imasnopn  14856  ispsmet  14880  ismet  14901  isxmet  14902  metn0  14935  xmetres2  14936  elbl3ps  14951  elbl3  14952  xblpnfps  14955  xblpnf  14956  elmopn2  15006  metss  15051  bdxmet  15058  metrest  15063  xmetxp  15064  xmetxpbl  15065  metcnp3  15068  metcnp  15069  metcnp2  15070  metcn  15071  txmetcnp  15075  txmetcn  15076  metcnpd  15077  bl2ioo  15107  addcncntoplem  15118  elcncf  15130  elcncf2  15131  ivthdec  15201  ellimc3apf  15217  cnlimcim  15228  dveflem  15283  ply1termlem  15299  sincosq2sgn  15384  sinq12gt0  15387  logltb  15431  ltexp2  15498  wilthlem1  15537  lgsdilem  15589  lgsdir2lem4  15593  lgsdir2  15595  lgsne0  15600  lgsabs1  15601  gausslemma2dlem3  15625  gausslemma2dlem7  15630  lgseisenlem3  15634  lgsquad3  15646  2lgslem1a  15650  2lgslem3c  15657  2lgslem3d  15658  2lgsoddprmlem4  15674  2sqlem7  15683  2sqlem8a  15684  uhgreq12g  15757  isuhgropm  15762  uhgr0e  15763  upgrop  15785  uhgrvtxedgiedgb  15817  cbvrald  15894  bj-nalset  16000  bj-sels  16019  bj-nnelirr  16058  isomninnlem  16141  iswomninnlem  16160  iswomni0  16162  ismkvnnlem  16163