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  449  anbi12d  456  orbi12d  739  con1biidc  804  pm4.54dc  838  dn1dc  901  dedlem0a  909  xorbi12d  1313  nbbndc  1325  eleq12d  2149  neeq12d  2265  neleq12d  2345  raleqbi1dv  2557  rexeqbi1dv  2558  reueqd  2559  rmoeqd  2560  raleqbidv  2561  rexeqbidv  2562  raleqbidva  2563  rexeqbidva  2564  eueq3dc  2766  sbc19.21g  2882  sbcabel  2895  sbcel1g  2925  sbceq1g  2926  sbcel2g  2927  sbceq2g  2928  sbccsb2g  2935  sbcco3g  2959  sseq12d  3028  raaanlem  3346  sbcssg  3350  ralsng  3433  2ralunsn  3590  csbunig  3609  disjeq12d  3775  breq123d  3799  sbcbr12g  3835  sbcbr1g  3836  sbcbr2g  3837  treq  3881  nalset  3908  copsex4g  4002  sucelon  4247  posng  4430  csbxpg  4439  sbcrel  4444  csbcnvg  4537  eliniseg  4715  brcodir  4732  csbrng  4802  sbcfung  4945  fneq12d  5011  feq12d  5056  feq123d  5057  sbcfng  5064  sbcfg  5065  f1osng  5187  csbfv12g  5230  funimass4  5245  dmfco  5262  eqfnfv  5286  eqfnfv2  5287  fneqeql2  5297  fvimacnvi  5302  funimass3  5304  fniniseg  5308  rexsupp  5312  unpreima  5313  ralrnmpt  5330  rexrnmpt  5331  dffo3  5335  fmptco  5351  fressnfv  5371  eufnfv  5410  fnunirn  5427  dff13  5428  f1elima  5433  cocan1  5447  cocan2  5448  fliftel  5453  fliftf  5459  isoresbr  5469  isoini  5477  f1oiso  5485  f1ofveu  5520  mpt2eq123dva  5586  ovid  5637  ov  5640  ovg  5659  ovelrn  5669  caovord2d  5690  ofrfval2  5747  offveqb  5750  eqop  5823  reldm  5832  f1od2  5876  mpt2xopoveq  5878  mpt2xopovel  5879  isprmpt2  5881  tpostpos  5902  smoiso  5940  frecsuclem3  6013  nnaordr  6106  nnaword  6107  nnaordex  6123  ereq1  6136  brdifun  6156  erth2  6174  qliftfun  6211  brecop  6219  dom2lem  6275  xpcomco  6323  php5fin  6366  supisolem  6421  inflbti  6437  ltapig  6528  ltmpig  6529  nlt1pig  6531  mulcmpblnq  6558  ltsonq  6588  lt2addnq  6594  lt2mulnq  6595  archnqq  6607  prarloclemarch  6608  ltrnqg  6610  mulcmpblnq0  6634  preqlu  6662  genpdflem  6697  addnqprllem  6717  addnqprulem  6718  addlocprlemgt  6724  appdivnq  6753  mulnqprl  6758  mulnqpru  6759  mullocprlem  6760  distrlem4prl  6774  distrlem4pru  6775  1idprl  6780  1idpru  6781  ltexprlemloc  6797  cauappcvgprlemladdrl  6847  cauappcvgprlemladd  6848  cauappcvgprlem1  6849  archrecnq  6853  caucvgprlemnkj  6856  caucvgprprlemexb  6897  addcmpblnr  6916  lttrsr  6939  ltsosr  6941  ltasrg  6947  mulextsr1  6957  srpospr  6959  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  ltresr  7007  axcaucvglemres  7065  cnegexlem1  7283  negeu  7299  subadd2  7312  subcan2  7333  addrsub  7475  ltaddneg  7528  ltaddnegr  7529  ltadd1  7533  leadd2  7535  ltsubadd  7536  lesubadd  7538  ltaddsub2  7541  leaddsub2  7543  ltaddpos  7556  lesub2  7561  ltsub2  7563  ltnegcon1  7567  ltnegcon2  7568  lenegcon1  7570  lenegcon2  7571  addge01  7576  addge02  7577  suble0  7580  leaddle0  7581  lesub0  7583  sublt0d  7670  recexre  7678  reaplt  7688  reapltxor  7689  reapneg  7697  remulext1  7699  apreim  7703  apcotr  7707  apadd2  7709  addext  7710  mulcanap2d  7752  diveqap0  7770  diveqap1  7793  ltmul2  7934  lemul2  7935  ltmulgt11  7942  ltmulgt12  7943  gt0div  7948  ge0div  7949  ltmuldiv  7952  ltrec1  7966  lerec2  7967  ledivdiv  7968  ltdiv23  7970  lediv23  7971  suprleubex  8032  creur  8036  creui  8037  nn1suc  8058  nnrecl  8286  znnsub  8402  zgt0ge1  8409  zltlen  8426  nn0n0n1ge2b  8427  btwnnz  8441  gtndiv  8442  prime  8446  eluz2  8625  indstr2  8696  negm  8700  nn01to3  8702  qapne  8724  qltlen  8725  qreccl  8727  divlt1lt  8801  divle1le  8802  nnledivrp  8837  iccid  8948  elioc2  8959  elico2  8960  elicc2  8961  elfz2  9036  fzen  9062  fzsubel  9078  elfzp1  9089  fzpr  9094  fzrevral2  9123  fzrevral3  9124  nn0disj  9148  2ffzeq  9151  fzosplitsni  9244  fvinim0ffz  9250  ioo0  9268  ico0  9270  ioc0  9271  modq0  9331  negqmod0  9333  zmodidfzo  9355  frecuzrdgfn  9414  nn0ennn  9425  sq11  9548  nn0le2msqd  9646  nn0opth2d  9650  2shfti  9719  cjap  9793  rexfiuz  9875  rexanuz2  9877  abs00ap  9948  absext  9949  sqabs  9968  abslt  9974  absle  9975  absdiflt  9978  absdifle  9979  lenegsq  9981  minmax  10112  ltmininf  10116  clim  10120  clim0c  10125  climrecvg1n  10185  dvdsval2  10198  zdvdsdc  10216  modmulconst  10227  dvdsaddr  10239  dvdsabseq  10247  fzocongeq  10258  zeo3  10267  odd2np1  10272  oddp1d2  10290  zob  10291  oddm1d2  10292  nnoddm1d2  10310  divalgb  10325  divalgmod  10327  modremain  10329  gcdn0gt0  10369  bezoutlemstep  10386  dvdssq  10420  nn0seqcvgd  10423  algcvgblem  10431  lcmdvds  10461  lcmgcdeq  10465  coprmdvds  10474  qredeq  10478  congr  10482  isprm2  10499  isprm3  10500  prmdvdsexp  10527  prmdvdsexpb  10528  prmexpb  10530  prmfac1  10531  cncongrprm  10536  oddpwdclemxy  10547  oddpwdclemodd  10550  cbvrald  10598  bj-nalset  10686  bj-sels  10705  bj-nnelirr  10748