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  458  anbi12d  465  orbi12d  783  con1biidc  863  pm4.54dc  888  dn1dc  945  dedlem0a  953  xorbi12d  1361  nbbndc  1373  eleq12d  2211  neeq12d  2329  neleq12d  2410  raleqbi1dv  2637  rexeqbi1dv  2638  reueqd  2639  rmoeqd  2640  raleqbidv  2641  rexeqbidv  2642  raleqbidva  2643  rexeqbidva  2644  eueq3dc  2862  sbc19.21g  2981  sbcabel  2994  sbcel1g  3026  sbceq1g  3027  sbcel2g  3028  sbceq2g  3029  sbccsb2g  3037  sbcco3g  3062  sseq12d  3133  raaanlem  3473  sbcssg  3477  ralsng  3571  2ralunsn  3733  csbunig  3752  disjeq12d  3923  breq123d  3951  sbcbr12g  3991  sbcbr1g  3992  sbcbr2g  3993  treq  4040  nalset  4066  exmidsssn  4133  copsex4g  4177  sucelon  4427  posng  4619  csbxpg  4628  sbcrel  4633  csbcnvg  4731  eliniseg  4917  brcodir  4934  csbrng  5008  sbcfung  5155  fneq12d  5223  feq12d  5270  feq123d  5271  sbcfng  5278  sbcfg  5279  f1osng  5416  csbfv12g  5465  funimass4  5480  dmfco  5497  eqfnfv  5526  eqfnfv2  5527  fneqeql2  5537  fvimacnvi  5542  funimass3  5544  fniniseg  5548  rexsupp  5552  unpreima  5553  ralrnmpt  5570  rexrnmpt  5571  dffo3  5575  fmptco  5594  fressnfv  5615  eufnfv  5656  foima2  5661  fnunirn  5676  dff13  5677  f1elima  5682  cocan1  5696  cocan2  5697  fliftel  5702  fliftf  5708  isoresbr  5718  isoini  5727  f1oiso  5735  f1ofveu  5770  mpoeq123dva  5840  ovid  5895  ov  5898  ovg  5917  ovelrn  5927  caovord2d  5948  ofrfval2  6006  offveqb  6009  eqop  6083  reldm  6092  f1od2  6140  mpoxopoveq  6145  mpoxopovel  6146  tpostpos  6169  smoiso  6207  frecabcl  6304  frecsuclem  6311  nnaordr  6414  nnaword  6415  nnaordex  6431  ereq1  6444  brdifun  6464  erth2  6482  qliftfun  6519  brecop  6527  elmapg  6563  elpmg  6566  dom2lem  6674  xpcomco  6728  php5fin  6784  elfi2  6868  supisolem  6903  inflbti  6919  inl11  6958  ismkvnex  7037  mkvprop  7040  exmidfodomrlemreseldju  7073  ltapig  7170  ltmpig  7171  nlt1pig  7173  mulcmpblnq  7200  ltsonq  7230  lt2addnq  7236  lt2mulnq  7237  archnqq  7249  prarloclemarch  7250  ltrnqg  7252  mulcmpblnq0  7276  preqlu  7304  genpdflem  7339  addnqprllem  7359  addnqprulem  7360  addlocprlemgt  7366  appdivnq  7395  mulnqprl  7400  mulnqpru  7401  mullocprlem  7402  distrlem4prl  7416  distrlem4pru  7417  1idprl  7422  1idpru  7423  ltexprlemloc  7439  cauappcvgprlemladdrl  7489  cauappcvgprlemladd  7490  cauappcvgprlem1  7491  archrecnq  7495  caucvgprlemnkj  7498  caucvgprprlemexb  7539  addcmpblnr  7571  lttrsr  7594  ltsosr  7596  ltasrg  7602  mulextsr1  7613  srpospr  7615  caucvgsrlemcau  7625  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  map2psrprg  7637  ltresr  7671  axcaucvglemres  7731  cnegexlem1  7961  negeu  7977  subadd2  7990  subcan2  8011  addrsub  8157  ltaddneg  8210  ltaddnegr  8211  ltadd1  8215  leadd2  8217  ltsubadd  8218  lesubadd  8220  ltaddsub2  8223  leaddsub2  8225  ltaddpos  8238  lesub2  8243  ltsub2  8245  ltnegcon1  8249  ltnegcon2  8250  lenegcon1  8252  lenegcon2  8253  addge01  8258  addge02  8259  suble0  8262  leaddle0  8263  lesub0  8265  eqord2  8270  sublt0d  8356  recexre  8364  reaplt  8374  reapltxor  8375  reapneg  8383  remulext1  8385  apreim  8389  apcotr  8393  apadd2  8395  addext  8396  apsub1  8428  mulcanap2d  8447  diveqap0  8466  diveqap1  8489  apmul2  8573  ltmul2  8638  lemul2  8639  ltmulgt11  8646  ltmulgt12  8647  gt0div  8652  ge0div  8653  ltmuldiv  8656  ltrec1  8670  lerec2  8671  ledivdiv  8672  ltdiv23  8674  lediv23  8675  suprleubex  8736  creur  8741  creui  8742  nn1suc  8763  nnrecl  8999  znnsub  9129  zgt0ge1  9136  zltlen  9153  nn0n0n1ge2b  9154  nn0le2is012  9157  btwnnz  9169  gtndiv  9170  prime  9174  eluz2  9356  indstr2  9430  negm  9434  nn01to3  9436  qapne  9458  qltlen  9459  qreccl  9461  divlt1lt  9541  divle1le  9542  nnledivrp  9583  xnn0xadd0  9680  xltadd2  9690  xsubge0  9694  xlesubadd  9696  iccid  9738  elioc2  9749  elico2  9750  elicc2  9751  elfz2  9828  fzen  9854  fzsubel  9871  elfzp1  9883  fzpr  9888  fzrevral2  9917  fzrevral3  9918  nn0disj  9946  2ffzeq  9949  fzosplitsni  10043  fvinim0ffz  10049  ioo0  10068  ico0  10070  ioc0  10071  modq0  10133  negqmod0  10135  zmodidfzo  10157  frecuzrdgtcl  10216  nn0ennn  10237  sq11  10396  nn0le2msqd  10497  nn0opth2d  10501  hashen  10562  zfz1isolem1  10615  zfz1iso  10616  2shfti  10635  cjap  10710  cnreim  10782  rexfiuz  10793  rexanuz2  10795  abs00ap  10866  absext  10867  sqabs  10886  abslt  10892  absle  10893  absdiflt  10896  absdifle  10897  lenegsq  10899  minmax  11033  ltmininf  11038  xrminmax  11066  xrmin1inf  11068  xrmin2inf  11069  xrltmininf  11071  xrlemininf  11072  clim  11082  clim0c  11087  climrecvg1n  11149  zsumdc  11185  fsum2dlemstep  11235  binomlem  11284  pwm1geoserap1  11309  zproddc  11380  efieq  11478  sin01bnd  11500  cos01bnd  11501  dvdsval2  11532  zdvdsdc  11550  modmulconst  11561  dvdsaddr  11573  dvdsabseq  11581  fzocongeq  11592  zeo3  11601  odd2np1  11606  oddp1d2  11623  zob  11624  oddm1d2  11625  nnoddm1d2  11643  divalgb  11658  divalgmod  11660  modremain  11662  gcdn0gt0  11702  bezoutlemstep  11721  dvdssq  11755  nn0seqcvgd  11758  algcvgblem  11766  lcmdvds  11796  lcmgcdeq  11800  coprmdvds  11809  qredeq  11813  congr  11817  isprm2  11834  isprm3  11835  prmdvdsexp  11862  prmdvdsexpb  11863  prmexpb  11865  prmfac1  11866  cncongrprm  11871  oddpwdclemxy  11883  oddpwdclemodd  11886  qnumdenbi  11906  qnumgt0  11912  hashdvds  11933  crth  11936  oddennn  11941  ctinfomlemom  11976  istopg  12205  eltg  12260  eltg2  12261  tgss2  12287  bastop1  12291  bastop2  12292  iscld  12311  isnei  12352  neiint  12353  iscn  12405  iscnp  12407  iscnp3  12411  tgcn  12416  ssidcn  12418  lmbr2  12422  lmbrf  12423  cnnei  12440  cnrest2  12444  eltx  12467  imasnopn  12507  ispsmet  12531  ismet  12552  isxmet  12553  metn0  12586  xmetres2  12587  elbl3ps  12602  elbl3  12603  xblpnfps  12606  xblpnf  12607  elmopn2  12657  metss  12702  bdxmet  12709  metrest  12714  xmetxp  12715  xmetxpbl  12716  metcnp3  12719  metcnp  12720  metcnp2  12721  metcn  12722  txmetcnp  12726  txmetcn  12727  metcnpd  12728  bl2ioo  12750  addcncntoplem  12759  elcncf  12768  elcncf2  12769  ivthdec  12830  ellimc3apf  12837  cnlimcim  12848  dveflem  12895  sincosq2sgn  12956  sinq12gt0  12959  logltb  13003  cbvrald  13166  bj-nalset  13264  bj-sels  13283  bj-nnelirr  13322  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419