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  3bior2fd  1365  xorbi12d  1401  nbbndc  1413  eleq12d  2275  neeq12d  2395  neleq12d  2476  raleqbi1dv  2713  rexeqbi1dv  2714  reueqd  2715  rmoeqd  2716  raleqbidv  2717  rexeqbidv  2718  raleqbidva  2719  rexeqbidva  2720  eueq3dc  2946  sbc19.21g  3066  sbcabel  3079  sbcel1g  3111  sbceq1g  3112  sbcel2g  3113  sbceq2g  3114  sbccsb2g  3122  sbcco3g  3150  sseq12d  3223  raaanlem  3564  sbcssg  3568  ralsng  3672  2ralunsn  3838  csbunig  3857  disjeq12d  4029  breq123d  4057  sbcbr12g  4098  sbcbr1g  4099  sbcbr2g  4100  treq  4147  nalset  4173  exmidsssn  4245  copsex4g  4290  onsucb  4550  posng  4746  csbxpg  4755  sbcrel  4760  csbcnvg  4861  eliniseg  5051  brcodir  5069  csbrng  5143  sbcfung  5294  fneq12d  5365  feq12d  5414  feq123d  5415  sbcfng  5422  sbcfg  5423  f1osng  5562  csbfv12g  5613  funimass4  5628  dmfco  5646  eqfnfv  5676  eqfnfv2  5677  fneqeql2  5688  fvimacnvi  5693  funimass3  5695  fniniseg  5699  rexsupp  5703  unpreima  5704  ralrnmpt  5721  rexrnmpt  5722  dffo3  5726  fmptco  5745  fressnfv  5770  eufnfv  5814  foima2  5819  fnunirn  5835  dff13  5836  f1elima  5841  cocan1  5855  cocan2  5856  fliftel  5861  fliftf  5867  isoresbr  5877  isoini  5886  f1oiso  5894  f1ofveu  5931  mpoeq123dva  6005  ovid  6061  ov  6064  ovg  6084  ovelrn  6094  caovord2d  6115  ofrfval2  6174  offveqb  6177  eqop  6262  reldm  6271  f1od2  6320  mpoxopoveq  6325  mpoxopovel  6326  tpostpos  6349  smoiso  6387  frecabcl  6484  frecsuclem  6491  nnaordr  6595  nnaword  6596  nnaordex  6613  ereq1  6626  brdifun  6646  erth2  6666  qliftfun  6703  brecop  6711  elmapg  6747  elpmg  6750  dom2lem  6862  xpcomco  6920  pw2f1odclem  6930  php5fin  6978  elfi2  7073  supisolem  7109  inflbti  7125  inl11  7166  ismkvnex  7256  mkvprop  7259  nninfwlporlemd  7273  exmidfodomrlemreseldju  7307  ltapig  7450  ltmpig  7451  nlt1pig  7453  mulcmpblnq  7480  ltsonq  7510  lt2addnq  7516  lt2mulnq  7517  archnqq  7529  prarloclemarch  7530  ltrnqg  7532  mulcmpblnq0  7556  preqlu  7584  genpdflem  7619  addnqprllem  7639  addnqprulem  7640  addlocprlemgt  7646  appdivnq  7675  mulnqprl  7680  mulnqpru  7681  mullocprlem  7682  distrlem4prl  7696  distrlem4pru  7697  1idprl  7702  1idpru  7703  ltexprlemloc  7719  cauappcvgprlemladdrl  7769  cauappcvgprlemladd  7770  cauappcvgprlem1  7771  archrecnq  7775  caucvgprlemnkj  7778  caucvgprprlemexb  7819  addcmpblnr  7851  lttrsr  7874  ltsosr  7876  ltasrg  7882  mulextsr1  7893  srpospr  7895  caucvgsrlemcau  7905  caucvgsrlemgt1  7907  caucvgsrlemoffres  7912  map2psrprg  7917  ltresr  7951  axcaucvglemres  8011  eqlelt  8158  cnegexlem1  8246  negeu  8262  subadd2  8275  subcan2  8296  addrsub  8442  ltaddneg  8496  ltaddnegr  8497  ltadd1  8501  leadd2  8503  ltsubadd  8504  lesubadd  8506  ltaddsub2  8509  leaddsub2  8511  ltaddpos  8524  lesub2  8529  ltsub2  8531  ltnegcon1  8535  ltnegcon2  8536  lenegcon1  8538  lenegcon2  8539  addge01  8544  addge02  8545  suble0  8548  leaddle0  8549  lesub0  8551  eqord2  8556  sublt0d  8642  recexre  8650  reaplt  8660  reapltxor  8661  reapneg  8669  remulext1  8671  apreim  8675  apcotr  8679  apadd2  8681  addext  8682  apsub1  8714  mulcanap2d  8734  diveqap0  8754  diveqap1  8777  apmul2  8861  ltmul2  8928  lemul2  8929  ltmulgt11  8936  ltmulgt12  8937  gt0div  8942  ge0div  8943  ltmuldiv  8946  ltrec1  8960  lerec2  8961  ledivdiv  8962  ltdiv23  8964  lediv23  8965  suprleubex  9026  creur  9031  creui  9032  nn1suc  9054  nnrecl  9292  znnsub  9423  zgt0ge1  9430  zltlen  9450  nn0n0n1ge2b  9451  nn0le2is012  9454  btwnnz  9466  gtndiv  9467  prime  9471  eluz2  9653  indstr2  9729  negm  9735  nn01to3  9737  qapne  9759  qltlen  9760  qreccl  9762  irrmulap  9768  divlt1lt  9845  divle1le  9846  nnledivrp  9887  xnn0xadd0  9988  xltadd2  9998  xsubge0  10002  xlesubadd  10004  iccid  10046  elioc2  10057  elico2  10058  elicc2  10059  elfz2  10136  fzen  10164  fzsubel  10181  elfzp1  10193  fzpr  10198  fzrevral2  10227  fzrevral3  10228  nn0disj  10259  2ffzeq  10262  fzosplitsni  10362  fvinim0ffz  10368  ioo0  10400  ico0  10402  ioc0  10403  modq0  10472  negqmod0  10474  zmodidfzo  10496  frecuzrdgtcl  10555  nn0ennn  10576  nninfinf  10586  sq11  10755  nn0le2msqd  10862  nn0opth2d  10866  hashen  10927  zfz1isolem1  10983  zfz1iso  10984  csbwrdg  11021  wrdnval  11022  eqwrd  11032  ccat0  11050  ccatws1lenp1bg  11087  2shfti  11113  cjap  11188  cnreim  11260  rexfiuz  11271  rexanuz2  11273  abs00ap  11344  absext  11345  sqabs  11364  abslt  11370  absle  11371  absdiflt  11374  absdifle  11375  lenegsq  11377  minmax  11512  ltmininf  11517  mingeb  11524  xrminmax  11547  xrmin1inf  11549  xrmin2inf  11550  xrltmininf  11552  xrlemininf  11553  clim  11563  clim0c  11568  climrecvg1n  11630  zsumdc  11666  fsum2dlemstep  11716  binomlem  11765  pwm1geoserap1  11790  zproddc  11861  efieq  12017  sin01bnd  12039  cos01bnd  12040  dvdsval2  12072  modm1div  12082  zdvdsdc  12094  modmulconst  12105  dvdsaddr  12119  dvdsabseq  12129  fzocongeq  12140  zeo3  12150  odd2np1  12155  oddp1d2  12172  zob  12173  oddm1d2  12174  nnoddm1d2  12192  divalgb  12207  divalgmod  12209  modremain  12211  bits0  12230  bitsp1e  12234  bitsp1o  12235  bitscmp  12240  bitsinv1lem  12243  gcdn0gt0  12270  bezoutlemstep  12289  dvdssq  12323  nn0seqcvgd  12334  algcvgblem  12342  lcmdvds  12372  lcmgcdeq  12376  coprmdvds  12385  qredeq  12389  congr  12393  isprm2  12410  isprm3  12411  prmdvdsexp  12441  prmdvdsexpb  12442  prmexpb  12444  prmfac1  12445  cncongrprm  12450  oddpwdclemxy  12462  oddpwdclemodd  12465  qnumdenbi  12485  qnumgt0  12491  hashdvds  12514  crth  12517  fermltl  12527  modprminveq  12544  pcpremul  12587  pc2dvds  12624  pcz  12626  prmpwdvds  12649  4sqlem16  12700  oddennn  12734  ctinfomlemom  12769  prdsbasmpt  13083  prdsbasmpt2  13091  mgm1  13173  ismhm  13264  mhmpropd  13269  issubm  13275  issubm2  13276  grpsubrcan  13384  grplactcnv  13405  grp1  13409  eqgval  13530  eqgid  13533  quselbasg  13537  isghm  13550  conjnmzb  13587  iscmn  13600  eqgabl  13637  rngmneg1  13680  rngmneg2  13681  rngpropd  13688  srgen1zr  13721  ringideu  13750  ringpropd  13771  crngpropd  13772  dvdsrd  13827  dvdsr02  13838  opprunitd  13843  crngunit  13844  unitpropdg  13881  rhmunitinv  13911  isnzr2  13917  issubrng  13932  resrhm2b  13982  aprval  14015  islmod  14024  islssm  14090  islssmg  14091  ellspsn  14150  isridl  14237  zrhrhmb  14355  zndvds  14382  znleval  14386  istopg  14442  eltg  14495  eltg2  14496  tgss2  14522  bastop1  14526  bastop2  14527  iscld  14546  isnei  14587  neiint  14588  iscn  14640  iscnp  14642  iscnp3  14646  tgcn  14651  ssidcn  14653  lmbr2  14657  lmbrf  14658  cnnei  14675  cnrest2  14679  eltx  14702  imasnopn  14742  ispsmet  14766  ismet  14787  isxmet  14788  metn0  14821  xmetres2  14822  elbl3ps  14837  elbl3  14838  xblpnfps  14841  xblpnf  14842  elmopn2  14892  metss  14937  bdxmet  14944  metrest  14949  xmetxp  14950  xmetxpbl  14951  metcnp3  14954  metcnp  14955  metcnp2  14956  metcn  14957  txmetcnp  14961  txmetcn  14962  metcnpd  14963  bl2ioo  14993  addcncntoplem  15004  elcncf  15016  elcncf2  15017  ivthdec  15087  ellimc3apf  15103  cnlimcim  15114  dveflem  15169  ply1termlem  15185  sincosq2sgn  15270  sinq12gt0  15273  logltb  15317  ltexp2  15384  wilthlem1  15423  lgsdilem  15475  lgsdir2lem4  15479  lgsdir2  15481  lgsne0  15486  lgsabs1  15487  gausslemma2dlem3  15511  gausslemma2dlem7  15516  lgseisenlem3  15520  lgsquad3  15532  2lgslem1a  15536  2lgslem3c  15543  2lgslem3d  15544  2lgsoddprmlem4  15560  2sqlem7  15569  2sqlem8a  15570  cbvrald  15686  bj-nalset  15793  bj-sels  15812  bj-nnelirr  15851  isomninnlem  15931  iswomninnlem  15950  iswomni0  15952  ismkvnnlem  15953