Theorem bitrd 188

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr2d  189  bitr3d  190  bitr4d  191  bitrid  192  bitrdi  196  3bitrd  214  3bitr2d  216  3bitr3d  218  3bitr4d  220  imbi12d  234  bibi12d  235  sylan9bb  462  anbi12d  473  orbi12d  794  con1biidc  878  pm4.54dc  903  dn1dc  962  dedlem0a  970  xorbi12d  1393  nbbndc  1405  eleq12d  2260  neeq12d  2380  neleq12d  2461  raleqbi1dv  2694  rexeqbi1dv  2695  reueqd  2696  rmoeqd  2697  raleqbidv  2698  rexeqbidv  2699  raleqbidva  2700  rexeqbidva  2701  eueq3dc  2926  sbc19.21g  3046  sbcabel  3059  sbcel1g  3091  sbceq1g  3092  sbcel2g  3093  sbceq2g  3094  sbccsb2g  3102  sbcco3g  3129  sseq12d  3201  raaanlem  3543  sbcssg  3547  ralsng  3650  2ralunsn  3816  csbunig  3835  disjeq12d  4007  breq123d  4035  sbcbr12g  4076  sbcbr1g  4077  sbcbr2g  4078  treq  4125  nalset  4151  exmidsssn  4223  copsex4g  4268  onsucb  4523  posng  4719  csbxpg  4728  sbcrel  4733  csbcnvg  4832  eliniseg  5019  brcodir  5037  csbrng  5111  sbcfung  5262  fneq12d  5330  feq12d  5377  feq123d  5378  sbcfng  5385  sbcfg  5386  f1osng  5524  csbfv12g  5575  funimass4  5590  dmfco  5608  eqfnfv  5637  eqfnfv2  5638  fneqeql2  5649  fvimacnvi  5654  funimass3  5656  fniniseg  5660  rexsupp  5664  unpreima  5665  ralrnmpt  5682  rexrnmpt  5683  dffo3  5687  fmptco  5706  fressnfv  5727  eufnfv  5771  foima2  5776  fnunirn  5792  dff13  5793  f1elima  5798  cocan1  5812  cocan2  5813  fliftel  5818  fliftf  5824  isoresbr  5834  isoini  5843  f1oiso  5851  f1ofveu  5888  mpoeq123dva  5961  ovid  6017  ov  6020  ovg  6039  ovelrn  6049  caovord2d  6070  ofrfval2  6127  offveqb  6130  eqop  6206  reldm  6215  f1od2  6264  mpoxopoveq  6269  mpoxopovel  6270  tpostpos  6293  smoiso  6331  frecabcl  6428  frecsuclem  6435  nnaordr  6539  nnaword  6540  nnaordex  6557  ereq1  6570  brdifun  6590  erth2  6610  qliftfun  6647  brecop  6655  elmapg  6691  elpmg  6694  dom2lem  6802  xpcomco  6856  pw2f1odclem  6866  php5fin  6914  elfi2  7005  supisolem  7041  inflbti  7057  inl11  7098  ismkvnex  7188  mkvprop  7191  nninfwlporlemd  7205  exmidfodomrlemreseldju  7234  ltapig  7372  ltmpig  7373  nlt1pig  7375  mulcmpblnq  7402  ltsonq  7432  lt2addnq  7438  lt2mulnq  7439  archnqq  7451  prarloclemarch  7452  ltrnqg  7454  mulcmpblnq0  7478  preqlu  7506  genpdflem  7541  addnqprllem  7561  addnqprulem  7562  addlocprlemgt  7568  appdivnq  7597  mulnqprl  7602  mulnqpru  7603  mullocprlem  7604  distrlem4prl  7618  distrlem4pru  7619  1idprl  7624  1idpru  7625  ltexprlemloc  7641  cauappcvgprlemladdrl  7691  cauappcvgprlemladd  7692  cauappcvgprlem1  7693  archrecnq  7697  caucvgprlemnkj  7700  caucvgprprlemexb  7741  addcmpblnr  7773  lttrsr  7796  ltsosr  7798  ltasrg  7804  mulextsr1  7815  srpospr  7817  caucvgsrlemcau  7827  caucvgsrlemgt1  7829  caucvgsrlemoffres  7834  map2psrprg  7839  ltresr  7873  axcaucvglemres  7933  eqlelt  8079  cnegexlem1  8167  negeu  8183  subadd2  8196  subcan2  8217  addrsub  8363  ltaddneg  8416  ltaddnegr  8417  ltadd1  8421  leadd2  8423  ltsubadd  8424  lesubadd  8426  ltaddsub2  8429  leaddsub2  8431  ltaddpos  8444  lesub2  8449  ltsub2  8451  ltnegcon1  8455  ltnegcon2  8456  lenegcon1  8458  lenegcon2  8459  addge01  8464  addge02  8465  suble0  8468  leaddle0  8469  lesub0  8471  eqord2  8476  sublt0d  8562  recexre  8570  reaplt  8580  reapltxor  8581  reapneg  8589  remulext1  8591  apreim  8595  apcotr  8599  apadd2  8601  addext  8602  apsub1  8634  mulcanap2d  8654  diveqap0  8674  diveqap1  8697  apmul2  8781  ltmul2  8848  lemul2  8849  ltmulgt11  8856  ltmulgt12  8857  gt0div  8862  ge0div  8863  ltmuldiv  8866  ltrec1  8880  lerec2  8881  ledivdiv  8882  ltdiv23  8884  lediv23  8885  suprleubex  8946  creur  8951  creui  8952  nn1suc  8973  nnrecl  9209  znnsub  9339  zgt0ge1  9346  zltlen  9366  nn0n0n1ge2b  9367  nn0le2is012  9370  btwnnz  9382  gtndiv  9383  prime  9387  eluz2  9569  indstr2  9645  negm  9651  nn01to3  9653  qapne  9675  qltlen  9676  qreccl  9678  divlt1lt  9760  divle1le  9761  nnledivrp  9802  xnn0xadd0  9903  xltadd2  9913  xsubge0  9917  xlesubadd  9919  iccid  9961  elioc2  9972  elico2  9973  elicc2  9974  elfz2  10051  fzen  10079  fzsubel  10096  elfzp1  10108  fzpr  10113  fzrevral2  10142  fzrevral3  10143  nn0disj  10174  2ffzeq  10177  fzosplitsni  10271  fvinim0ffz  10277  ioo0  10296  ico0  10298  ioc0  10299  modq0  10366  negqmod0  10368  zmodidfzo  10390  frecuzrdgtcl  10449  nn0ennn  10470  nninfinf  10480  sq11  10633  nn0le2msqd  10740  nn0opth2d  10744  hashen  10805  zfz1isolem1  10861  zfz1iso  10862  2shfti  10881  cjap  10956  cnreim  11028  rexfiuz  11039  rexanuz2  11041  abs00ap  11112  absext  11113  sqabs  11132  abslt  11138  absle  11139  absdiflt  11142  absdifle  11143  lenegsq  11145  minmax  11279  ltmininf  11284  mingeb  11291  xrminmax  11314  xrmin1inf  11316  xrmin2inf  11317  xrltmininf  11319  xrlemininf  11320  clim  11330  clim0c  11335  climrecvg1n  11397  zsumdc  11433  fsum2dlemstep  11483  binomlem  11532  pwm1geoserap1  11557  zproddc  11628  efieq  11784  sin01bnd  11806  cos01bnd  11807  dvdsval2  11838  modm1div  11848  zdvdsdc  11860  modmulconst  11871  dvdsaddr  11885  dvdsabseq  11894  fzocongeq  11905  zeo3  11914  odd2np1  11919  oddp1d2  11936  zob  11937  oddm1d2  11938  nnoddm1d2  11956  divalgb  11971  divalgmod  11973  modremain  11975  gcdn0gt0  12020  bezoutlemstep  12039  dvdssq  12073  nn0seqcvgd  12084  algcvgblem  12092  lcmdvds  12122  lcmgcdeq  12126  coprmdvds  12135  qredeq  12139  congr  12143  isprm2  12160  isprm3  12161  prmdvdsexp  12191  prmdvdsexpb  12192  prmexpb  12194  prmfac1  12195  cncongrprm  12200  oddpwdclemxy  12212  oddpwdclemodd  12215  qnumdenbi  12235  qnumgt0  12241  hashdvds  12264  crth  12267  fermltl  12277  modprminveq  12293  pcpremul  12336  pc2dvds  12373  pcz  12375  prmpwdvds  12398  4sqlem16  12449  oddennn  12454  ctinfomlemom  12489  mgm1  12857  ismhm  12936  mhmpropd  12941  issubm  12947  issubm2  12948  grpsubrcan  13048  grplactcnv  13069  grp1  13073  eqgval  13187  eqgid  13190  quselbasg  13194  isghm  13207  conjnmzb  13244  iscmn  13257  eqgabl  13292  rngmneg1  13326  rngmneg2  13327  rngpropd  13334  srgen1zr  13367  ringideu  13396  ringpropd  13417  crngpropd  13418  dvdsrd  13469  dvdsr02  13480  opprunitd  13485  crngunit  13486  unitpropdg  13523  rhmunitinv  13553  issubrng  13571  aprval  13623  islmod  13632  islssm  13698  islssmg  13699  lspsnel  13758  isridl  13844  zrhrhmb  13944  istopg  13984  eltg  14037  eltg2  14038  tgss2  14064  bastop1  14068  bastop2  14069  iscld  14088  isnei  14129  neiint  14130  iscn  14182  iscnp  14184  iscnp3  14188  tgcn  14193  ssidcn  14195  lmbr2  14199  lmbrf  14200  cnnei  14217  cnrest2  14221  eltx  14244  imasnopn  14284  ispsmet  14308  ismet  14329  isxmet  14330  metn0  14363  xmetres2  14364  elbl3ps  14379  elbl3  14380  xblpnfps  14383  xblpnf  14384  elmopn2  14434  metss  14479  bdxmet  14486  metrest  14491  xmetxp  14492  xmetxpbl  14493  metcnp3  14496  metcnp  14497  metcnp2  14498  metcn  14499  txmetcnp  14503  txmetcn  14504  metcnpd  14505  bl2ioo  14527  addcncntoplem  14536  elcncf  14545  elcncf2  14546  ivthdec  14607  ellimc3apf  14614  cnlimcim  14625  dveflem  14672  sincosq2sgn  14733  sinq12gt0  14736  logltb  14780  ltexp2  14845  wilthlem1  14883  lgsdilem  14914  lgsdir2lem4  14918  lgsdir2  14920  lgsne0  14925  lgsabs1  14926  2lgsoddprmlem4  14946  2sqlem7  14954  2sqlem8a  14955  cbvrald  15026  bj-nalset  15133  bj-sels  15152  bj-nnelirr  15191  isomninnlem  15266  iswomninnlem  15285  iswomni0  15287  ismkvnnlem  15288