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  2shfti  11084  cjap  11159  cnreim  11231  rexfiuz  11242  rexanuz2  11244  abs00ap  11315  absext  11316  sqabs  11335  abslt  11341  absle  11342  absdiflt  11345  absdifle  11346  lenegsq  11348  minmax  11483  ltmininf  11488  mingeb  11495  xrminmax  11518  xrmin1inf  11520  xrmin2inf  11521  xrltmininf  11523  xrlemininf  11524  clim  11534  clim0c  11539  climrecvg1n  11601  zsumdc  11637  fsum2dlemstep  11687  binomlem  11736  pwm1geoserap1  11761  zproddc  11832  efieq  11988  sin01bnd  12010  cos01bnd  12011  dvdsval2  12043  modm1div  12053  zdvdsdc  12065  modmulconst  12076  dvdsaddr  12090  dvdsabseq  12100  fzocongeq  12111  zeo3  12121  odd2np1  12126  oddp1d2  12143  zob  12144  oddm1d2  12145  nnoddm1d2  12163  divalgb  12178  divalgmod  12180  modremain  12182  bits0  12201  bitsp1e  12205  bitsp1o  12206  bitscmp  12211  bitsinv1lem  12214  gcdn0gt0  12241  bezoutlemstep  12260  dvdssq  12294  nn0seqcvgd  12305  algcvgblem  12313  lcmdvds  12343  lcmgcdeq  12347  coprmdvds  12356  qredeq  12360  congr  12364  isprm2  12381  isprm3  12382  prmdvdsexp  12412  prmdvdsexpb  12413  prmexpb  12415  prmfac1  12416  cncongrprm  12421  oddpwdclemxy  12433  oddpwdclemodd  12436  qnumdenbi  12456  qnumgt0  12462  hashdvds  12485  crth  12488  fermltl  12498  modprminveq  12515  pcpremul  12558  pc2dvds  12595  pcz  12597  prmpwdvds  12620  4sqlem16  12671  oddennn  12705  ctinfomlemom  12740  prdsbasmpt  13054  prdsbasmpt2  13062  mgm1  13144  ismhm  13235  mhmpropd  13240  issubm  13246  issubm2  13247  grpsubrcan  13355  grplactcnv  13376  grp1  13380  eqgval  13501  eqgid  13504  quselbasg  13508  isghm  13521  conjnmzb  13558  iscmn  13571  eqgabl  13608  rngmneg1  13651  rngmneg2  13652  rngpropd  13659  srgen1zr  13692  ringideu  13721  ringpropd  13742  crngpropd  13743  dvdsrd  13798  dvdsr02  13809  opprunitd  13814  crngunit  13815  unitpropdg  13852  rhmunitinv  13882  isnzr2  13888  issubrng  13903  resrhm2b  13953  aprval  13986  islmod  13995  islssm  14061  islssmg  14062  ellspsn  14121  isridl  14208  zrhrhmb  14326  zndvds  14353  znleval  14357  istopg  14413  eltg  14466  eltg2  14467  tgss2  14493  bastop1  14497  bastop2  14498  iscld  14517  isnei  14558  neiint  14559  iscn  14611  iscnp  14613  iscnp3  14617  tgcn  14622  ssidcn  14624  lmbr2  14628  lmbrf  14629  cnnei  14646  cnrest2  14650  eltx  14673  imasnopn  14713  ispsmet  14737  ismet  14758  isxmet  14759  metn0  14792  xmetres2  14793  elbl3ps  14808  elbl3  14809  xblpnfps  14812  xblpnf  14813  elmopn2  14863  metss  14908  bdxmet  14915  metrest  14920  xmetxp  14921  xmetxpbl  14922  metcnp3  14925  metcnp  14926  metcnp2  14927  metcn  14928  txmetcnp  14932  txmetcn  14933  metcnpd  14934  bl2ioo  14964  addcncntoplem  14975  elcncf  14987  elcncf2  14988  ivthdec  15058  ellimc3apf  15074  cnlimcim  15085  dveflem  15140  ply1termlem  15156  sincosq2sgn  15241  sinq12gt0  15244  logltb  15288  ltexp2  15355  wilthlem1  15394  lgsdilem  15446  lgsdir2lem4  15450  lgsdir2  15452  lgsne0  15457  lgsabs1  15458  gausslemma2dlem3  15482  gausslemma2dlem7  15487  lgseisenlem3  15491  lgsquad3  15503  2lgslem1a  15507  2lgslem3c  15514  2lgslem3d  15515  2lgsoddprmlem4  15531  2sqlem7  15540  2sqlem8a  15541  cbvrald  15657  bj-nalset  15764  bj-sels  15783  bj-nnelirr  15822  isomninnlem  15902  iswomninnlem  15921  iswomni0  15923  ismkvnnlem  15924