Theorem bitrd 187

Description: Deduction form of bitri 183. (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 179	. . 3 |- ( ( ph -> ps ) <-> ( ph -> ch ) )
3		bitrd.2	. . . 4 |- ( ph -> ( ch <-> th ) )
4	3	pm5.74i 179	. . 3 |- ( ( ph -> ch ) <-> ( ph -> th ) )
5	2, 4	bitri 183	. 2 |- ( ( ph -> ps ) <-> ( ph -> th ) )
6	5	pm5.74ri 180	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr2d  188  bitr3d  189  bitr4d  190  syl5bb  191  syl6bb  195  3bitrd  213  3bitr2d  215  3bitr3d  217  3bitr4d  219  imbi12d  233  bibi12d  234  sylan9bb  457  anbi12d  464  orbi12d  782  con1biidc  862  pm4.54dc  887  dn1dc  944  dedlem0a  952  xorbi12d  1360  nbbndc  1372  eleq12d  2210  neeq12d  2328  neleq12d  2409  raleqbi1dv  2634  rexeqbi1dv  2635  reueqd  2636  rmoeqd  2637  raleqbidv  2638  rexeqbidv  2639  raleqbidva  2640  rexeqbidva  2641  eueq3dc  2858  sbc19.21g  2977  sbcabel  2990  sbcel1g  3021  sbceq1g  3022  sbcel2g  3023  sbceq2g  3024  sbccsb2g  3032  sbcco3g  3057  sseq12d  3128  raaanlem  3468  sbcssg  3472  ralsng  3564  2ralunsn  3725  csbunig  3744  disjeq12d  3915  breq123d  3943  sbcbr12g  3983  sbcbr1g  3984  sbcbr2g  3985  treq  4032  nalset  4058  exmidsssn  4125  copsex4g  4169  sucelon  4419  posng  4611  csbxpg  4620  sbcrel  4625  csbcnvg  4723  eliniseg  4909  brcodir  4926  csbrng  5000  sbcfung  5147  fneq12d  5215  feq12d  5262  feq123d  5263  sbcfng  5270  sbcfg  5271  f1osng  5408  csbfv12g  5457  funimass4  5472  dmfco  5489  eqfnfv  5518  eqfnfv2  5519  fneqeql2  5529  fvimacnvi  5534  funimass3  5536  fniniseg  5540  rexsupp  5544  unpreima  5545  ralrnmpt  5562  rexrnmpt  5563  dffo3  5567  fmptco  5586  fressnfv  5607  eufnfv  5648  foima2  5653  fnunirn  5668  dff13  5669  f1elima  5674  cocan1  5688  cocan2  5689  fliftel  5694  fliftf  5700  isoresbr  5710  isoini  5719  f1oiso  5727  f1ofveu  5762  mpoeq123dva  5832  ovid  5887  ov  5890  ovg  5909  ovelrn  5919  caovord2d  5940  ofrfval2  5998  offveqb  6001  eqop  6075  reldm  6084  f1od2  6132  mpoxopoveq  6137  mpoxopovel  6138  tpostpos  6161  smoiso  6199  frecabcl  6296  frecsuclem  6303  nnaordr  6406  nnaword  6407  nnaordex  6423  ereq1  6436  brdifun  6456  erth2  6474  qliftfun  6511  brecop  6519  elmapg  6555  elpmg  6558  dom2lem  6666  xpcomco  6720  php5fin  6776  elfi2  6860  supisolem  6895  inflbti  6911  inl11  6950  ismkvnex  7029  mkvprop  7032  exmidfodomrlemreseldju  7056  ltapig  7146  ltmpig  7147  nlt1pig  7149  mulcmpblnq  7176  ltsonq  7206  lt2addnq  7212  lt2mulnq  7213  archnqq  7225  prarloclemarch  7226  ltrnqg  7228  mulcmpblnq0  7252  preqlu  7280  genpdflem  7315  addnqprllem  7335  addnqprulem  7336  addlocprlemgt  7342  appdivnq  7371  mulnqprl  7376  mulnqpru  7377  mullocprlem  7378  distrlem4prl  7392  distrlem4pru  7393  1idprl  7398  1idpru  7399  ltexprlemloc  7415  cauappcvgprlemladdrl  7465  cauappcvgprlemladd  7466  cauappcvgprlem1  7467  archrecnq  7471  caucvgprlemnkj  7474  caucvgprprlemexb  7515  addcmpblnr  7547  lttrsr  7570  ltsosr  7572  ltasrg  7578  mulextsr1  7589  srpospr  7591  caucvgsrlemcau  7601  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  map2psrprg  7613  ltresr  7647  axcaucvglemres  7707  cnegexlem1  7937  negeu  7953  subadd2  7966  subcan2  7987  addrsub  8133  ltaddneg  8186  ltaddnegr  8187  ltadd1  8191  leadd2  8193  ltsubadd  8194  lesubadd  8196  ltaddsub2  8199  leaddsub2  8201  ltaddpos  8214  lesub2  8219  ltsub2  8221  ltnegcon1  8225  ltnegcon2  8226  lenegcon1  8228  lenegcon2  8229  addge01  8234  addge02  8235  suble0  8238  leaddle0  8239  lesub0  8241  eqord2  8246  sublt0d  8332  recexre  8340  reaplt  8350  reapltxor  8351  reapneg  8359  remulext1  8361  apreim  8365  apcotr  8369  apadd2  8371  addext  8372  apsub1  8404  mulcanap2d  8423  diveqap0  8442  diveqap1  8465  apmul2  8549  ltmul2  8614  lemul2  8615  ltmulgt11  8622  ltmulgt12  8623  gt0div  8628  ge0div  8629  ltmuldiv  8632  ltrec1  8646  lerec2  8647  ledivdiv  8648  ltdiv23  8650  lediv23  8651  suprleubex  8712  creur  8717  creui  8718  nn1suc  8739  nnrecl  8975  znnsub  9105  zgt0ge1  9112  zltlen  9129  nn0n0n1ge2b  9130  nn0le2is012  9133  btwnnz  9145  gtndiv  9146  prime  9150  eluz2  9332  indstr2  9403  negm  9407  nn01to3  9409  qapne  9431  qltlen  9432  qreccl  9434  divlt1lt  9511  divle1le  9512  nnledivrp  9553  xnn0xadd0  9650  xltadd2  9660  xsubge0  9664  xlesubadd  9666  iccid  9708  elioc2  9719  elico2  9720  elicc2  9721  elfz2  9797  fzen  9823  fzsubel  9840  elfzp1  9852  fzpr  9857  fzrevral2  9886  fzrevral3  9887  nn0disj  9915  2ffzeq  9918  fzosplitsni  10012  fvinim0ffz  10018  ioo0  10037  ico0  10039  ioc0  10040  modq0  10102  negqmod0  10104  zmodidfzo  10126  frecuzrdgtcl  10185  nn0ennn  10206  sq11  10365  nn0le2msqd  10465  nn0opth2d  10469  hashen  10530  zfz1isolem1  10583  zfz1iso  10584  2shfti  10603  cjap  10678  cnreim  10750  rexfiuz  10761  rexanuz2  10763  abs00ap  10834  absext  10835  sqabs  10854  abslt  10860  absle  10861  absdiflt  10864  absdifle  10865  lenegsq  10867  minmax  11001  ltmininf  11006  xrminmax  11034  xrmin1inf  11036  xrmin2inf  11037  xrltmininf  11039  xrlemininf  11040  clim  11050  clim0c  11055  climrecvg1n  11117  zsumdc  11153  fsum2dlemstep  11203  binomlem  11252  pwm1geoserap1  11277  efieq  11442  sin01bnd  11464  cos01bnd  11465  dvdsval2  11496  zdvdsdc  11514  modmulconst  11525  dvdsaddr  11537  dvdsabseq  11545  fzocongeq  11556  zeo3  11565  odd2np1  11570  oddp1d2  11587  zob  11588  oddm1d2  11589  nnoddm1d2  11607  divalgb  11622  divalgmod  11624  modremain  11626  gcdn0gt0  11666  bezoutlemstep  11685  dvdssq  11719  nn0seqcvgd  11722  algcvgblem  11730  lcmdvds  11760  lcmgcdeq  11764  coprmdvds  11773  qredeq  11777  congr  11781  isprm2  11798  isprm3  11799  prmdvdsexp  11826  prmdvdsexpb  11827  prmexpb  11829  prmfac1  11830  cncongrprm  11835  oddpwdclemxy  11847  oddpwdclemodd  11850  qnumdenbi  11870  qnumgt0  11876  hashdvds  11897  crth  11900  oddennn  11905  ctinfomlemom  11940  istopg  12166  eltg  12221  eltg2  12222  tgss2  12248  bastop1  12252  bastop2  12253  iscld  12272  isnei  12313  neiint  12314  iscn  12366  iscnp  12368  iscnp3  12372  tgcn  12377  ssidcn  12379  lmbr2  12383  lmbrf  12384  cnnei  12401  cnrest2  12405  eltx  12428  imasnopn  12468  ispsmet  12492  ismet  12513  isxmet  12514  metn0  12547  xmetres2  12548  elbl3ps  12563  elbl3  12564  xblpnfps  12567  xblpnf  12568  elmopn2  12618  metss  12663  bdxmet  12670  metrest  12675  xmetxp  12676  xmetxpbl  12677  metcnp3  12680  metcnp  12681  metcnp2  12682  metcn  12683  txmetcnp  12687  txmetcn  12688  metcnpd  12689  bl2ioo  12711  addcncntoplem  12720  elcncf  12729  elcncf2  12730  ivthdec  12791  ellimc3apf  12798  cnlimcim  12809  dveflem  12855  sincosq2sgn  12908  sinq12gt0  12911  cbvrald  12995  bj-nalset  13093  bj-sels  13112  bj-nnelirr  13151  isomninnlem  13225