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  795  con1biidc  879  pm4.54dc  904  dn1dc  963  dedlem0a  971  3bior2fd  1366  xorbi12d  1402  nbbndc  1414  eleq12d  2278  neeq12d  2398  neleq12d  2479  raleqbi1dv  2717  rexeqbi1dv  2718  reueqd  2719  rmoeqd  2720  raleqbidv  2721  rexeqbidv  2722  raleqbidva  2723  rexeqbidva  2724  eueq3dc  2954  sbc19.21g  3074  sbcabel  3088  sbcel1g  3120  sbceq1g  3121  sbcel2g  3122  sbceq2g  3123  sbccsb2g  3131  sbcco3g  3159  sseq12d  3232  raaanlem  3573  sbcssg  3577  ralsng  3683  2ralunsn  3853  csbunig  3872  disjeq12d  4044  breq123d  4073  sbcbr12g  4115  sbcbr1g  4116  sbcbr2g  4117  treq  4164  nalset  4190  exmidsssn  4262  copsex4g  4309  onsucb  4569  posng  4765  csbxpg  4774  sbcrel  4779  csbcnvg  4880  eliniseg  5071  brcodir  5089  csbrng  5163  sbcfung  5314  fneq12d  5385  feq12d  5435  feq123d  5436  sbcfng  5443  sbcfg  5444  f1osng  5586  csbfv12g  5637  funimass4  5652  dmfco  5670  eqfnfv  5700  eqfnfv2  5701  fneqeql2  5712  fvimacnvi  5717  funimass3  5719  fniniseg  5723  rexsupp  5727  unpreima  5728  ralrnmpt  5745  rexrnmpt  5746  dffo3  5750  fmptco  5769  fressnfv  5794  eufnfv  5838  foima2  5843  fnunirn  5859  dff13  5860  f1elima  5865  cocan1  5879  cocan2  5880  fliftel  5885  fliftf  5891  isoresbr  5901  isoini  5910  f1oiso  5918  f1ofveu  5955  mpoeq123dva  6029  ovid  6085  ov  6088  ovg  6108  ovelrn  6118  caovord2d  6139  ofrfval2  6198  offveqb  6201  eqop  6286  reldm  6295  f1od2  6344  mpoxopoveq  6349  mpoxopovel  6350  tpostpos  6373  smoiso  6411  frecabcl  6508  frecsuclem  6515  nnaordr  6619  nnaword  6620  nnaordex  6637  ereq1  6650  brdifun  6670  erth2  6690  qliftfun  6727  brecop  6735  elmapg  6771  elpmg  6774  dom2lem  6886  xpcomco  6946  pw2f1odclem  6956  php5fin  7005  elfi2  7100  supisolem  7136  inflbti  7152  inl11  7193  ismkvnex  7283  mkvprop  7286  nninfwlporlemd  7300  exmidfodomrlemreseldju  7339  ltapig  7486  ltmpig  7487  nlt1pig  7489  mulcmpblnq  7516  ltsonq  7546  lt2addnq  7552  lt2mulnq  7553  archnqq  7565  prarloclemarch  7566  ltrnqg  7568  mulcmpblnq0  7592  preqlu  7620  genpdflem  7655  addnqprllem  7675  addnqprulem  7676  addlocprlemgt  7682  appdivnq  7711  mulnqprl  7716  mulnqpru  7717  mullocprlem  7718  distrlem4prl  7732  distrlem4pru  7733  1idprl  7738  1idpru  7739  ltexprlemloc  7755  cauappcvgprlemladdrl  7805  cauappcvgprlemladd  7806  cauappcvgprlem1  7807  archrecnq  7811  caucvgprlemnkj  7814  caucvgprprlemexb  7855  addcmpblnr  7887  lttrsr  7910  ltsosr  7912  ltasrg  7918  mulextsr1  7929  srpospr  7931  caucvgsrlemcau  7941  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  map2psrprg  7953  ltresr  7987  axcaucvglemres  8047  eqlelt  8194  cnegexlem1  8282  negeu  8298  subadd2  8311  subcan2  8332  addrsub  8478  ltaddneg  8532  ltaddnegr  8533  ltadd1  8537  leadd2  8539  ltsubadd  8540  lesubadd  8542  ltaddsub2  8545  leaddsub2  8547  ltaddpos  8560  lesub2  8565  ltsub2  8567  ltnegcon1  8571  ltnegcon2  8572  lenegcon1  8574  lenegcon2  8575  addge01  8580  addge02  8581  suble0  8584  leaddle0  8585  lesub0  8587  eqord2  8592  sublt0d  8678  recexre  8686  reaplt  8696  reapltxor  8697  reapneg  8705  remulext1  8707  apreim  8711  apcotr  8715  apadd2  8717  addext  8718  apsub1  8750  mulcanap2d  8770  diveqap0  8790  diveqap1  8813  apmul2  8897  ltmul2  8964  lemul2  8965  ltmulgt11  8972  ltmulgt12  8973  gt0div  8978  ge0div  8979  ltmuldiv  8982  ltrec1  8996  lerec2  8997  ledivdiv  8998  ltdiv23  9000  lediv23  9001  suprleubex  9062  creur  9067  creui  9068  nn1suc  9090  nnrecl  9328  znnsub  9459  zgt0ge1  9466  zltlen  9486  nn0n0n1ge2b  9487  nn0le2is012  9490  btwnnz  9502  gtndiv  9503  prime  9507  eluz2  9689  indstr2  9765  negm  9771  nn01to3  9773  qapne  9795  qltlen  9796  qreccl  9798  irrmulap  9804  divlt1lt  9881  divle1le  9882  nnledivrp  9923  xnn0xadd0  10024  xltadd2  10034  xsubge0  10038  xlesubadd  10040  iccid  10082  elioc2  10093  elico2  10094  elicc2  10095  elfz2  10172  fzen  10200  fzsubel  10217  elfzp1  10229  fzpr  10234  fzrevral2  10263  fzrevral3  10264  nn0disj  10295  2ffzeq  10298  fzosplitsni  10401  fvinim0ffz  10407  ioo0  10439  ico0  10441  ioc0  10442  modq0  10511  negqmod0  10513  zmodidfzo  10535  frecuzrdgtcl  10594  nn0ennn  10615  nninfinf  10625  sq11  10794  nn0le2msqd  10901  nn0opth2d  10905  hashen  10966  zfz1isolem1  11022  zfz1iso  11023  csbwrdg  11060  wrdnval  11061  eqwrd  11071  ccat0  11090  ccatws1lenp1bg  11127  swrd0g  11151  swrdspsleq  11158  pfxeq  11187  pfxsuffeqwrdeq  11189  pfxsuff1eqwrdeq  11190  ccatopth2  11208  wrd2ind  11214  2shfti  11257  cjap  11332  cnreim  11404  rexfiuz  11415  rexanuz2  11417  abs00ap  11488  absext  11489  sqabs  11508  abslt  11514  absle  11515  absdiflt  11518  absdifle  11519  lenegsq  11521  minmax  11656  ltmininf  11661  mingeb  11668  xrminmax  11691  xrmin1inf  11693  xrmin2inf  11694  xrltmininf  11696  xrlemininf  11697  clim  11707  clim0c  11712  climrecvg1n  11774  zsumdc  11810  fsum2dlemstep  11860  binomlem  11909  pwm1geoserap1  11934  zproddc  12005  efieq  12161  sin01bnd  12183  cos01bnd  12184  dvdsval2  12216  modm1div  12226  zdvdsdc  12238  modmulconst  12249  dvdsaddr  12263  dvdsabseq  12273  fzocongeq  12284  zeo3  12294  odd2np1  12299  oddp1d2  12316  zob  12317  oddm1d2  12318  nnoddm1d2  12336  divalgb  12351  divalgmod  12353  modremain  12355  bits0  12374  bitsp1e  12378  bitsp1o  12379  bitscmp  12384  bitsinv1lem  12387  gcdn0gt0  12414  bezoutlemstep  12433  dvdssq  12467  nn0seqcvgd  12478  algcvgblem  12486  lcmdvds  12516  lcmgcdeq  12520  coprmdvds  12529  qredeq  12533  congr  12537  isprm2  12554  isprm3  12555  prmdvdsexp  12585  prmdvdsexpb  12586  prmexpb  12588  prmfac1  12589  cncongrprm  12594  oddpwdclemxy  12606  oddpwdclemodd  12609  qnumdenbi  12629  qnumgt0  12635  hashdvds  12658  crth  12661  fermltl  12671  modprminveq  12688  pcpremul  12731  pc2dvds  12768  pcz  12770  prmpwdvds  12793  4sqlem16  12844  oddennn  12878  ctinfomlemom  12913  prdsbasmpt  13227  prdsbasmpt2  13235  mgm1  13317  ismhm  13408  mhmpropd  13413  issubm  13419  issubm2  13420  grpsubrcan  13528  grplactcnv  13549  grp1  13553  eqgval  13674  eqgid  13677  quselbasg  13681  isghm  13694  conjnmzb  13731  iscmn  13744  eqgabl  13781  rngmneg1  13824  rngmneg2  13825  rngpropd  13832  srgen1zr  13865  ringideu  13894  ringpropd  13915  crngpropd  13916  dvdsrd  13971  dvdsr02  13982  opprunitd  13987  crngunit  13988  unitpropdg  14025  rhmunitinv  14055  isnzr2  14061  issubrng  14076  resrhm2b  14126  aprval  14159  islmod  14168  islssm  14234  islssmg  14235  ellspsn  14294  isridl  14381  zrhrhmb  14499  zndvds  14526  znleval  14530  istopg  14586  eltg  14639  eltg2  14640  tgss2  14666  bastop1  14670  bastop2  14671  iscld  14690  isnei  14731  neiint  14732  iscn  14784  iscnp  14786  iscnp3  14790  tgcn  14795  ssidcn  14797  lmbr2  14801  lmbrf  14802  cnnei  14819  cnrest2  14823  eltx  14846  imasnopn  14886  ispsmet  14910  ismet  14931  isxmet  14932  metn0  14965  xmetres2  14966  elbl3ps  14981  elbl3  14982  xblpnfps  14985  xblpnf  14986  elmopn2  15036  metss  15081  bdxmet  15088  metrest  15093  xmetxp  15094  xmetxpbl  15095  metcnp3  15098  metcnp  15099  metcnp2  15100  metcn  15101  txmetcnp  15105  txmetcn  15106  metcnpd  15107  bl2ioo  15137  addcncntoplem  15148  elcncf  15160  elcncf2  15161  ivthdec  15231  ellimc3apf  15247  cnlimcim  15258  dveflem  15313  ply1termlem  15329  sincosq2sgn  15414  sinq12gt0  15417  logltb  15461  ltexp2  15528  wilthlem1  15567  lgsdilem  15619  lgsdir2lem4  15623  lgsdir2  15625  lgsne0  15630  lgsabs1  15631  gausslemma2dlem3  15655  gausslemma2dlem7  15660  lgseisenlem3  15664  lgsquad3  15676  2lgslem1a  15680  2lgslem3c  15687  2lgslem3d  15688  2lgsoddprmlem4  15704  2sqlem7  15713  2sqlem8a  15714  uhgreq12g  15787  isuhgropm  15792  uhgr0e  15793  upgrop  15815  uhgrvtxedgiedgb  15847  cbvrald  15924  bj-nalset  16030  bj-sels  16049  bj-nnelirr  16088  isomninnlem  16171  iswomninnlem  16190  iswomni0  16192  ismkvnnlem  16193