Theorem bitrd 186

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bitr2d  187  bitr3d  188  bitr4d  189  syl5bb  190  syl6bb  194  3bitrd  212  3bitr2d  214  3bitr3d  216  3bitr4d  218  imbi12d  232  bibi12d  233  sylan9bb  450  anbi12d  457  orbi12d  740  con1biidc  807  pm4.54dc  841  dn1dc  904  dedlem0a  912  xorbi12d  1316  nbbndc  1328  eleq12d  2155  neeq12d  2271  neleq12d  2352  raleqbi1dv  2566  rexeqbi1dv  2567  reueqd  2568  rmoeqd  2569  raleqbidv  2570  rexeqbidv  2571  raleqbidva  2572  rexeqbidva  2573  eueq3dc  2780  sbc19.21g  2896  sbcabel  2909  sbcel1g  2939  sbceq1g  2940  sbcel2g  2941  sbceq2g  2942  sbccsb2g  2949  sbcco3g  2974  sseq12d  3044  raaanlem  3374  sbcssg  3378  ralsng  3466  2ralunsn  3625  csbunig  3644  disjeq12d  3810  breq123d  3834  sbcbr12g  3870  sbcbr1g  3871  sbcbr2g  3872  treq  3917  nalset  3944  copsex4g  4048  sucelon  4293  posng  4478  csbxpg  4487  sbcrel  4492  csbcnvg  4588  eliniseg  4769  brcodir  4786  csbrng  4858  sbcfung  5004  fneq12d  5071  feq12d  5116  feq123d  5117  sbcfng  5124  sbcfg  5125  f1osng  5257  csbfv12g  5303  funimass4  5318  dmfco  5335  eqfnfv  5360  eqfnfv2  5361  fneqeql2  5371  fvimacnvi  5376  funimass3  5378  fniniseg  5382  rexsupp  5386  unpreima  5387  ralrnmpt  5404  rexrnmpt  5405  dffo3  5409  fmptco  5427  fressnfv  5447  eufnfv  5486  foima2  5491  fnunirn  5507  dff13  5508  f1elima  5513  cocan1  5527  cocan2  5528  fliftel  5533  fliftf  5539  isoresbr  5549  isoini  5558  f1oiso  5566  f1ofveu  5601  mpt2eq123dva  5667  ovid  5718  ov  5721  ovg  5740  ovelrn  5750  caovord2d  5771  ofrfval2  5828  offveqb  5831  eqop  5904  reldm  5913  f1od2  5957  mpt2xopoveq  5959  mpt2xopovel  5960  isprmpt2  5962  tpostpos  5983  smoiso  6021  frecabcl  6118  frecsuclem  6125  nnaordr  6221  nnaword  6222  nnaordex  6238  ereq1  6251  brdifun  6271  erth2  6289  qliftfun  6326  brecop  6334  elmapg  6370  elpmg  6373  dom2lem  6441  xpcomco  6494  php5fin  6550  supisolem  6647  inflbti  6663  exmidfodomrlemreseldju  6770  ltapig  6841  ltmpig  6842  nlt1pig  6844  mulcmpblnq  6871  ltsonq  6901  lt2addnq  6907  lt2mulnq  6908  archnqq  6920  prarloclemarch  6921  ltrnqg  6923  mulcmpblnq0  6947  preqlu  6975  genpdflem  7010  addnqprllem  7030  addnqprulem  7031  addlocprlemgt  7037  appdivnq  7066  mulnqprl  7071  mulnqpru  7072  mullocprlem  7073  distrlem4prl  7087  distrlem4pru  7088  1idprl  7093  1idpru  7094  ltexprlemloc  7110  cauappcvgprlemladdrl  7160  cauappcvgprlemladd  7161  cauappcvgprlem1  7162  archrecnq  7166  caucvgprlemnkj  7169  caucvgprprlemexb  7210  addcmpblnr  7229  lttrsr  7252  ltsosr  7254  ltasrg  7260  mulextsr1  7270  srpospr  7272  caucvgsrlemcau  7282  caucvgsrlemgt1  7284  caucvgsrlemoffres  7289  ltresr  7320  axcaucvglemres  7378  cnegexlem1  7601  negeu  7617  subadd2  7630  subcan2  7651  addrsub  7793  ltaddneg  7846  ltaddnegr  7847  ltadd1  7851  leadd2  7853  ltsubadd  7854  lesubadd  7856  ltaddsub2  7859  leaddsub2  7861  ltaddpos  7874  lesub2  7879  ltsub2  7881  ltnegcon1  7885  ltnegcon2  7886  lenegcon1  7888  lenegcon2  7889  addge01  7894  addge02  7895  suble0  7898  leaddle0  7899  lesub0  7901  sublt0d  7988  recexre  7996  reaplt  8006  reapltxor  8007  reapneg  8015  remulext1  8017  apreim  8021  apcotr  8025  apadd2  8027  addext  8028  mulcanap2d  8070  diveqap0  8088  diveqap1  8111  ltmul2  8252  lemul2  8253  ltmulgt11  8260  ltmulgt12  8261  gt0div  8266  ge0div  8267  ltmuldiv  8270  ltrec1  8284  lerec2  8285  ledivdiv  8286  ltdiv23  8288  lediv23  8289  suprleubex  8350  creur  8354  creui  8355  nn1suc  8376  nnrecl  8604  znnsub  8734  zgt0ge1  8741  zltlen  8758  nn0n0n1ge2b  8759  btwnnz  8773  gtndiv  8774  prime  8778  eluz2  8957  indstr2  9028  negm  9032  nn01to3  9034  qapne  9056  qltlen  9057  qreccl  9059  divlt1lt  9133  divle1le  9134  nnledivrp  9169  iccid  9275  elioc2  9286  elico2  9287  elicc2  9288  elfz2  9363  fzen  9389  fzsubel  9405  elfzp1  9416  fzpr  9421  fzrevral2  9450  fzrevral3  9451  nn0disj  9477  2ffzeq  9480  fzosplitsni  9574  fvinim0ffz  9580  ioo0  9599  ico0  9601  ioc0  9602  modq0  9664  negqmod0  9666  zmodidfzo  9688  frecuzrdgtcl  9747  nn0ennn  9768  sq11  9925  nn0le2msqd  10023  nn0opth2d  10027  hashen  10088  zfz1isolem1  10141  zfz1iso  10142  2shfti  10161  cjap  10235  rexfiuz  10317  rexanuz2  10319  abs00ap  10390  absext  10391  sqabs  10410  abslt  10416  absle  10417  absdiflt  10420  absdifle  10421  lenegsq  10423  minmax  10554  ltmininf  10558  clim  10562  clim0c  10567  climrecvg1n  10627  zisum  10663  dvdsval2  10674  zdvdsdc  10692  modmulconst  10703  dvdsaddr  10715  dvdsabseq  10723  fzocongeq  10734  zeo3  10743  odd2np1  10748  oddp1d2  10765  zob  10766  oddm1d2  10767  nnoddm1d2  10785  divalgb  10800  divalgmod  10802  modremain  10804  gcdn0gt0  10844  bezoutlemstep  10861  dvdssq  10895  nn0seqcvgd  10898  algcvgblem  10906  lcmdvds  10936  lcmgcdeq  10940  coprmdvds  10949  qredeq  10953  congr  10957  isprm2  10974  isprm3  10975  prmdvdsexp  11002  prmdvdsexpb  11003  prmexpb  11005  prmfac1  11006  cncongrprm  11011  oddpwdclemxy  11022  oddpwdclemodd  11025  qnumdenbi  11045  qnumgt0  11051  hashdvds  11072  crth  11075  oddennn  11080  cbvrald  11126  bj-nalset  11224  bj-sels  11243  bj-nnelirr  11286