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  bitrdi  195  3bitrd  213  3bitr2d  215  3bitr3d  217  3bitr4d  219  imbi12d  233  bibi12d  234  sylan9bb  459  anbi12d  470  orbi12d  788  con1biidc  872  pm4.54dc  897  dn1dc  955  dedlem0a  963  xorbi12d  1377  nbbndc  1389  eleq12d  2241  neeq12d  2360  neleq12d  2441  raleqbi1dv  2673  rexeqbi1dv  2674  reueqd  2675  rmoeqd  2676  raleqbidv  2677  rexeqbidv  2678  raleqbidva  2679  rexeqbidva  2680  eueq3dc  2904  sbc19.21g  3023  sbcabel  3036  sbcel1g  3068  sbceq1g  3069  sbcel2g  3070  sbceq2g  3071  sbccsb2g  3079  sbcco3g  3106  sseq12d  3178  raaanlem  3520  sbcssg  3524  ralsng  3623  2ralunsn  3785  csbunig  3804  disjeq12d  3975  breq123d  4003  sbcbr12g  4044  sbcbr1g  4045  sbcbr2g  4046  treq  4093  nalset  4119  exmidsssn  4188  copsex4g  4232  sucelon  4487  posng  4683  csbxpg  4692  sbcrel  4697  csbcnvg  4795  eliniseg  4981  brcodir  4998  csbrng  5072  sbcfung  5222  fneq12d  5290  feq12d  5337  feq123d  5338  sbcfng  5345  sbcfg  5346  f1osng  5483  csbfv12g  5532  funimass4  5547  dmfco  5564  eqfnfv  5593  eqfnfv2  5594  fneqeql2  5605  fvimacnvi  5610  funimass3  5612  fniniseg  5616  rexsupp  5620  unpreima  5621  ralrnmpt  5638  rexrnmpt  5639  dffo3  5643  fmptco  5662  fressnfv  5683  eufnfv  5726  foima2  5731  fnunirn  5746  dff13  5747  f1elima  5752  cocan1  5766  cocan2  5767  fliftel  5772  fliftf  5778  isoresbr  5788  isoini  5797  f1oiso  5805  f1ofveu  5841  mpoeq123dva  5914  ovid  5969  ov  5972  ovg  5991  ovelrn  6001  caovord2d  6022  ofrfval2  6077  offveqb  6080  eqop  6156  reldm  6165  f1od2  6214  mpoxopoveq  6219  mpoxopovel  6220  tpostpos  6243  smoiso  6281  frecabcl  6378  frecsuclem  6385  nnaordr  6489  nnaword  6490  nnaordex  6507  ereq1  6520  brdifun  6540  erth2  6558  qliftfun  6595  brecop  6603  elmapg  6639  elpmg  6642  dom2lem  6750  xpcomco  6804  php5fin  6860  elfi2  6949  supisolem  6985  inflbti  7001  inl11  7042  ismkvnex  7131  mkvprop  7134  nninfwlporlemd  7148  exmidfodomrlemreseldju  7177  ltapig  7300  ltmpig  7301  nlt1pig  7303  mulcmpblnq  7330  ltsonq  7360  lt2addnq  7366  lt2mulnq  7367  archnqq  7379  prarloclemarch  7380  ltrnqg  7382  mulcmpblnq0  7406  preqlu  7434  genpdflem  7469  addnqprllem  7489  addnqprulem  7490  addlocprlemgt  7496  appdivnq  7525  mulnqprl  7530  mulnqpru  7531  mullocprlem  7532  distrlem4prl  7546  distrlem4pru  7547  1idprl  7552  1idpru  7553  ltexprlemloc  7569  cauappcvgprlemladdrl  7619  cauappcvgprlemladd  7620  cauappcvgprlem1  7621  archrecnq  7625  caucvgprlemnkj  7628  caucvgprprlemexb  7669  addcmpblnr  7701  lttrsr  7724  ltsosr  7726  ltasrg  7732  mulextsr1  7743  srpospr  7745  caucvgsrlemcau  7755  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  map2psrprg  7767  ltresr  7801  axcaucvglemres  7861  eqlelt  8006  cnegexlem1  8094  negeu  8110  subadd2  8123  subcan2  8144  addrsub  8290  ltaddneg  8343  ltaddnegr  8344  ltadd1  8348  leadd2  8350  ltsubadd  8351  lesubadd  8353  ltaddsub2  8356  leaddsub2  8358  ltaddpos  8371  lesub2  8376  ltsub2  8378  ltnegcon1  8382  ltnegcon2  8383  lenegcon1  8385  lenegcon2  8386  addge01  8391  addge02  8392  suble0  8395  leaddle0  8396  lesub0  8398  eqord2  8403  sublt0d  8489  recexre  8497  reaplt  8507  reapltxor  8508  reapneg  8516  remulext1  8518  apreim  8522  apcotr  8526  apadd2  8528  addext  8529  apsub1  8561  mulcanap2d  8580  diveqap0  8599  diveqap1  8622  apmul2  8706  ltmul2  8772  lemul2  8773  ltmulgt11  8780  ltmulgt12  8781  gt0div  8786  ge0div  8787  ltmuldiv  8790  ltrec1  8804  lerec2  8805  ledivdiv  8806  ltdiv23  8808  lediv23  8809  suprleubex  8870  creur  8875  creui  8876  nn1suc  8897  nnrecl  9133  znnsub  9263  zgt0ge1  9270  zltlen  9290  nn0n0n1ge2b  9291  nn0le2is012  9294  btwnnz  9306  gtndiv  9307  prime  9311  eluz2  9493  indstr2  9568  negm  9574  nn01to3  9576  qapne  9598  qltlen  9599  qreccl  9601  divlt1lt  9681  divle1le  9682  nnledivrp  9723  xnn0xadd0  9824  xltadd2  9834  xsubge0  9838  xlesubadd  9840  iccid  9882  elioc2  9893  elico2  9894  elicc2  9895  elfz2  9972  fzen  9999  fzsubel  10016  elfzp1  10028  fzpr  10033  fzrevral2  10062  fzrevral3  10063  nn0disj  10094  2ffzeq  10097  fzosplitsni  10191  fvinim0ffz  10197  ioo0  10216  ico0  10218  ioc0  10219  modq0  10285  negqmod0  10287  zmodidfzo  10309  frecuzrdgtcl  10368  nn0ennn  10389  sq11  10548  nn0le2msqd  10653  nn0opth2d  10657  hashen  10718  zfz1isolem1  10775  zfz1iso  10776  2shfti  10795  cjap  10870  cnreim  10942  rexfiuz  10953  rexanuz2  10955  abs00ap  11026  absext  11027  sqabs  11046  abslt  11052  absle  11053  absdiflt  11056  absdifle  11057  lenegsq  11059  minmax  11193  ltmininf  11198  mingeb  11205  xrminmax  11228  xrmin1inf  11230  xrmin2inf  11231  xrltmininf  11233  xrlemininf  11234  clim  11244  clim0c  11249  climrecvg1n  11311  zsumdc  11347  fsum2dlemstep  11397  binomlem  11446  pwm1geoserap1  11471  zproddc  11542  efieq  11698  sin01bnd  11720  cos01bnd  11721  dvdsval2  11752  modm1div  11762  zdvdsdc  11774  modmulconst  11785  dvdsaddr  11799  dvdsabseq  11807  fzocongeq  11818  zeo3  11827  odd2np1  11832  oddp1d2  11849  zob  11850  oddm1d2  11851  nnoddm1d2  11869  divalgb  11884  divalgmod  11886  modremain  11888  gcdn0gt0  11933  bezoutlemstep  11952  dvdssq  11986  nn0seqcvgd  11995  algcvgblem  12003  lcmdvds  12033  lcmgcdeq  12037  coprmdvds  12046  qredeq  12050  congr  12054  isprm2  12071  isprm3  12072  prmdvdsexp  12102  prmdvdsexpb  12103  prmexpb  12105  prmfac1  12106  cncongrprm  12111  oddpwdclemxy  12123  oddpwdclemodd  12126  qnumdenbi  12146  qnumgt0  12152  hashdvds  12175  crth  12178  fermltl  12188  modprminveq  12204  pcpremul  12247  pc2dvds  12283  pcz  12285  prmpwdvds  12307  oddennn  12347  ctinfomlemom  12382  mgm1  12624  ismhm  12685  mhmpropd  12689  issubm  12695  istopg  12791  eltg  12846  eltg2  12847  tgss2  12873  bastop1  12877  bastop2  12878  iscld  12897  isnei  12938  neiint  12939  iscn  12991  iscnp  12993  iscnp3  12997  tgcn  13002  ssidcn  13004  lmbr2  13008  lmbrf  13009  cnnei  13026  cnrest2  13030  eltx  13053  imasnopn  13093  ispsmet  13117  ismet  13138  isxmet  13139  metn0  13172  xmetres2  13173  elbl3ps  13188  elbl3  13189  xblpnfps  13192  xblpnf  13193  elmopn2  13243  metss  13288  bdxmet  13295  metrest  13300  xmetxp  13301  xmetxpbl  13302  metcnp3  13305  metcnp  13306  metcnp2  13307  metcn  13308  txmetcnp  13312  txmetcn  13313  metcnpd  13314  bl2ioo  13336  addcncntoplem  13345  elcncf  13354  elcncf2  13355  ivthdec  13416  ellimc3apf  13423  cnlimcim  13434  dveflem  13481  sincosq2sgn  13542  sinq12gt0  13545  logltb  13589  ltexp2  13654  lgsdilem  13722  lgsdir2lem4  13726  lgsdir2  13728  lgsne0  13733  lgsabs1  13734  2sqlem7  13751  2sqlem8a  13752  cbvrald  13823  bj-nalset  13930  bj-sels  13949  bj-nnelirr  13988  isomninnlem  14062  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084