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  2267  neeq12d  2387  neleq12d  2468  raleqbi1dv  2705  rexeqbi1dv  2706  reueqd  2707  rmoeqd  2708  raleqbidv  2709  rexeqbidv  2710  raleqbidva  2711  rexeqbidva  2712  eueq3dc  2938  sbc19.21g  3058  sbcabel  3071  sbcel1g  3103  sbceq1g  3104  sbcel2g  3105  sbceq2g  3106  sbccsb2g  3114  sbcco3g  3142  sseq12d  3215  raaanlem  3556  sbcssg  3560  ralsng  3663  2ralunsn  3829  csbunig  3848  disjeq12d  4020  breq123d  4048  sbcbr12g  4089  sbcbr1g  4090  sbcbr2g  4091  treq  4138  nalset  4164  exmidsssn  4236  copsex4g  4281  onsucb  4540  posng  4736  csbxpg  4745  sbcrel  4750  csbcnvg  4851  eliniseg  5040  brcodir  5058  csbrng  5132  sbcfung  5283  fneq12d  5351  feq12d  5400  feq123d  5401  sbcfng  5408  sbcfg  5409  f1osng  5548  csbfv12g  5599  funimass4  5614  dmfco  5632  eqfnfv  5662  eqfnfv2  5663  fneqeql2  5674  fvimacnvi  5679  funimass3  5681  fniniseg  5685  rexsupp  5689  unpreima  5690  ralrnmpt  5707  rexrnmpt  5708  dffo3  5712  fmptco  5731  fressnfv  5752  eufnfv  5796  foima2  5801  fnunirn  5817  dff13  5818  f1elima  5823  cocan1  5837  cocan2  5838  fliftel  5843  fliftf  5849  isoresbr  5859  isoini  5868  f1oiso  5876  f1ofveu  5913  mpoeq123dva  5987  ovid  6043  ov  6046  ovg  6066  ovelrn  6076  caovord2d  6097  ofrfval2  6156  offveqb  6159  eqop  6244  reldm  6253  f1od2  6302  mpoxopoveq  6307  mpoxopovel  6308  tpostpos  6331  smoiso  6369  frecabcl  6466  frecsuclem  6473  nnaordr  6577  nnaword  6578  nnaordex  6595  ereq1  6608  brdifun  6628  erth2  6648  qliftfun  6685  brecop  6693  elmapg  6729  elpmg  6732  dom2lem  6840  xpcomco  6894  pw2f1odclem  6904  php5fin  6952  elfi2  7047  supisolem  7083  inflbti  7099  inl11  7140  ismkvnex  7230  mkvprop  7233  nninfwlporlemd  7247  exmidfodomrlemreseldju  7279  ltapig  7422  ltmpig  7423  nlt1pig  7425  mulcmpblnq  7452  ltsonq  7482  lt2addnq  7488  lt2mulnq  7489  archnqq  7501  prarloclemarch  7502  ltrnqg  7504  mulcmpblnq0  7528  preqlu  7556  genpdflem  7591  addnqprllem  7611  addnqprulem  7612  addlocprlemgt  7618  appdivnq  7647  mulnqprl  7652  mulnqpru  7653  mullocprlem  7654  distrlem4prl  7668  distrlem4pru  7669  1idprl  7674  1idpru  7675  ltexprlemloc  7691  cauappcvgprlemladdrl  7741  cauappcvgprlemladd  7742  cauappcvgprlem1  7743  archrecnq  7747  caucvgprlemnkj  7750  caucvgprprlemexb  7791  addcmpblnr  7823  lttrsr  7846  ltsosr  7848  ltasrg  7854  mulextsr1  7865  srpospr  7867  caucvgsrlemcau  7877  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  map2psrprg  7889  ltresr  7923  axcaucvglemres  7983  eqlelt  8130  cnegexlem1  8218  negeu  8234  subadd2  8247  subcan2  8268  addrsub  8414  ltaddneg  8468  ltaddnegr  8469  ltadd1  8473  leadd2  8475  ltsubadd  8476  lesubadd  8478  ltaddsub2  8481  leaddsub2  8483  ltaddpos  8496  lesub2  8501  ltsub2  8503  ltnegcon1  8507  ltnegcon2  8508  lenegcon1  8510  lenegcon2  8511  addge01  8516  addge02  8517  suble0  8520  leaddle0  8521  lesub0  8523  eqord2  8528  sublt0d  8614  recexre  8622  reaplt  8632  reapltxor  8633  reapneg  8641  remulext1  8643  apreim  8647  apcotr  8651  apadd2  8653  addext  8654  apsub1  8686  mulcanap2d  8706  diveqap0  8726  diveqap1  8749  apmul2  8833  ltmul2  8900  lemul2  8901  ltmulgt11  8908  ltmulgt12  8909  gt0div  8914  ge0div  8915  ltmuldiv  8918  ltrec1  8932  lerec2  8933  ledivdiv  8934  ltdiv23  8936  lediv23  8937  suprleubex  8998  creur  9003  creui  9004  nn1suc  9026  nnrecl  9264  znnsub  9394  zgt0ge1  9401  zltlen  9421  nn0n0n1ge2b  9422  nn0le2is012  9425  btwnnz  9437  gtndiv  9438  prime  9442  eluz2  9624  indstr2  9700  negm  9706  nn01to3  9708  qapne  9730  qltlen  9731  qreccl  9733  irrmulap  9739  divlt1lt  9816  divle1le  9817  nnledivrp  9858  xnn0xadd0  9959  xltadd2  9969  xsubge0  9973  xlesubadd  9975  iccid  10017  elioc2  10028  elico2  10029  elicc2  10030  elfz2  10107  fzen  10135  fzsubel  10152  elfzp1  10164  fzpr  10169  fzrevral2  10198  fzrevral3  10199  nn0disj  10230  2ffzeq  10233  fzosplitsni  10328  fvinim0ffz  10334  ioo0  10366  ico0  10368  ioc0  10369  modq0  10438  negqmod0  10440  zmodidfzo  10462  frecuzrdgtcl  10521  nn0ennn  10542  nninfinf  10552  sq11  10721  nn0le2msqd  10828  nn0opth2d  10832  hashen  10893  zfz1isolem1  10949  zfz1iso  10950  csbwrdg  10981  wrdnval  10982  eqwrd  10992  2shfti  11013  cjap  11088  cnreim  11160  rexfiuz  11171  rexanuz2  11173  abs00ap  11244  absext  11245  sqabs  11264  abslt  11270  absle  11271  absdiflt  11274  absdifle  11275  lenegsq  11277  minmax  11412  ltmininf  11417  mingeb  11424  xrminmax  11447  xrmin1inf  11449  xrmin2inf  11450  xrltmininf  11452  xrlemininf  11453  clim  11463  clim0c  11468  climrecvg1n  11530  zsumdc  11566  fsum2dlemstep  11616  binomlem  11665  pwm1geoserap1  11690  zproddc  11761  efieq  11917  sin01bnd  11939  cos01bnd  11940  dvdsval2  11972  modm1div  11982  zdvdsdc  11994  modmulconst  12005  dvdsaddr  12019  dvdsabseq  12029  fzocongeq  12040  zeo3  12050  odd2np1  12055  oddp1d2  12072  zob  12073  oddm1d2  12074  nnoddm1d2  12092  divalgb  12107  divalgmod  12109  modremain  12111  bits0  12130  bitsp1e  12134  bitsp1o  12135  bitscmp  12140  bitsinv1lem  12143  gcdn0gt0  12170  bezoutlemstep  12189  dvdssq  12223  nn0seqcvgd  12234  algcvgblem  12242  lcmdvds  12272  lcmgcdeq  12276  coprmdvds  12285  qredeq  12289  congr  12293  isprm2  12310  isprm3  12311  prmdvdsexp  12341  prmdvdsexpb  12342  prmexpb  12344  prmfac1  12345  cncongrprm  12350  oddpwdclemxy  12362  oddpwdclemodd  12365  qnumdenbi  12385  qnumgt0  12391  hashdvds  12414  crth  12417  fermltl  12427  modprminveq  12444  pcpremul  12487  pc2dvds  12524  pcz  12526  prmpwdvds  12549  4sqlem16  12600  oddennn  12634  ctinfomlemom  12669  prdsbasmpt  12982  prdsbasmpt2  12990  mgm1  13072  ismhm  13163  mhmpropd  13168  issubm  13174  issubm2  13175  grpsubrcan  13283  grplactcnv  13304  grp1  13308  eqgval  13429  eqgid  13432  quselbasg  13436  isghm  13449  conjnmzb  13486  iscmn  13499  eqgabl  13536  rngmneg1  13579  rngmneg2  13580  rngpropd  13587  srgen1zr  13620  ringideu  13649  ringpropd  13670  crngpropd  13671  dvdsrd  13726  dvdsr02  13737  opprunitd  13742  crngunit  13743  unitpropdg  13780  rhmunitinv  13810  isnzr2  13816  issubrng  13831  resrhm2b  13881  aprval  13914  islmod  13923  islssm  13989  islssmg  13990  ellspsn  14049  isridl  14136  zrhrhmb  14254  zndvds  14281  znleval  14285  istopg  14319  eltg  14372  eltg2  14373  tgss2  14399  bastop1  14403  bastop2  14404  iscld  14423  isnei  14464  neiint  14465  iscn  14517  iscnp  14519  iscnp3  14523  tgcn  14528  ssidcn  14530  lmbr2  14534  lmbrf  14535  cnnei  14552  cnrest2  14556  eltx  14579  imasnopn  14619  ispsmet  14643  ismet  14664  isxmet  14665  metn0  14698  xmetres2  14699  elbl3ps  14714  elbl3  14715  xblpnfps  14718  xblpnf  14719  elmopn2  14769  metss  14814  bdxmet  14821  metrest  14826  xmetxp  14827  xmetxpbl  14828  metcnp3  14831  metcnp  14832  metcnp2  14833  metcn  14834  txmetcnp  14838  txmetcn  14839  metcnpd  14840  bl2ioo  14870  addcncntoplem  14881  elcncf  14893  elcncf2  14894  ivthdec  14964  ellimc3apf  14980  cnlimcim  14991  dveflem  15046  ply1termlem  15062  sincosq2sgn  15147  sinq12gt0  15150  logltb  15194  ltexp2  15261  wilthlem1  15300  lgsdilem  15352  lgsdir2lem4  15356  lgsdir2  15358  lgsne0  15363  lgsabs1  15364  gausslemma2dlem3  15388  gausslemma2dlem7  15393  lgseisenlem3  15397  lgsquad3  15409  2lgslem1a  15413  2lgslem3c  15420  2lgslem3d  15421  2lgsoddprmlem4  15437  2sqlem7  15446  2sqlem8a  15447  cbvrald  15518  bj-nalset  15625  bj-sels  15644  bj-nnelirr  15683  isomninnlem  15761  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783