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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bitr2d  189  bitr3d  190  bitr4d  191  bitrid  192  bitrdi  196  3bitrd  214  3bitr2d  216  3bitr3d  218  3bitr4d  220  imbi12d  234  bibi12d  235  sylan9bb  466  anbi12d  477  orbi12d  805  con1biidc  889  pm4.54dc  914  dn1dc  973  dedlem0a  981  dfifp3dc  995  dfifp4dc  996  dfifp5dc  997  3bior2fd  1395  xorbi12d  1431  nbbndc  1443  eleq12d  2309  neeq12d  2440  neleq12d  2521  raleqbi1dv  2761  rexeqbi1dv  2762  reueqd  2763  rmoeqd  2764  raleqbidv  2765  rexeqbidv  2766  raleqbidva  2767  rexeqbidva  2768  eueq3dc  3000  sbc19.21g  3120  sbcabel  3134  sbcel1g  3166  sbceq1g  3167  sbcel2g  3168  sbceq2g  3169  sbccsb2g  3177  sbcco3g  3205  sseq12d  3279  raaanlem  3632  sbcssg  3636  ralsng  3749  2ralunsn  3924  csbunig  3943  disjeq12d  4115  breq123d  4144  sbcbr12g  4186  sbcbr1g  4187  sbcbr2g  4188  treq  4235  nalset  4263  exmidsssn  4339  copsex4g  4387  onsucb  4650  posng  4847  csbxpg  4856  sbcrel  4861  csbcnvg  4964  eliniseg  5157  brcodir  5175  csbrng  5249  sbcfung  5401  fneq12d  5473  feq12d  5523  feq123d  5524  sbcfng  5531  sbcfg  5532  f1osng  5682  csbfv12g  5736  funimass4  5753  dmfco  5773  eqfnfv  5806  eqfnfv2  5807  fneqeql2  5818  fvimacnvi  5823  funimass3  5825  fniniseg  5829  unpreima  5833  ralrnmpt  5850  rexrnmpt  5851  dffo3  5855  fmptco  5874  fressnfv  5902  eufnfv  5949  foima2  5957  fnunirn  5973  dff13  5974  f1elima  5979  cocan1  5993  cocan2  5994  fliftel  5999  fliftf  6005  isoresbr  6015  isoini  6024  f1oiso  6032  f1ofveu  6073  mpoeq123dva  6149  ovid  6205  ov  6208  ovg  6228  ovelrn  6238  caovord2d  6259  ofrfval2  6319  offveqb  6322  eqop  6411  reldm  6420  f1od2  6471  suppval1  6479  suppssrst  6501  suppssrgst  6502  mpoxopoveq  6511  mpoxopovel  6512  tpostpos  6535  smoiso  6573  frecabcl  6670  frecsuclem  6677  nnaordr  6783  nnaword  6784  nnaordex  6801  ereq1  6814  brdifun  6834  erth2  6854  qliftfun  6891  brecop  6899  elmapg  6935  elpmg  6938  mapsnd  6970  dom2lem  7058  xpcomco  7124  pw2f1odclem  7134  php5fin  7186  funisfsupp  7291  ffsuppbi  7300  elfi2  7306  supisolem  7348  inflbti  7364  inl11  7405  ismkvnex  7495  mkvprop  7498  nninfwlporlemd  7512  exmidfodomrlemreseldju  7552  ltapig  7705  ltmpig  7706  nlt1pig  7708  mulcmpblnq  7735  ltsonq  7765  lt2addnq  7771  lt2mulnq  7772  archnqq  7784  prarloclemarch  7785  ltrnqg  7787  mulcmpblnq0  7811  preqlu  7839  genpdflem  7874  addnqprllem  7894  addnqprulem  7895  addlocprlemgt  7901  appdivnq  7930  mulnqprl  7935  mulnqpru  7936  mullocprlem  7937  distrlem4prl  7951  distrlem4pru  7952  1idprl  7957  1idpru  7958  ltexprlemloc  7974  cauappcvgprlemladdrl  8024  cauappcvgprlemladd  8025  cauappcvgprlem1  8026  archrecnq  8030  caucvgprlemnkj  8033  caucvgprprlemexb  8074  addcmpblnr  8106  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1  8148  srpospr  8150  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  map2psrprg  8172  ltresr  8206  axcaucvglemres  8266  eqlelt  8412  cnegexlem1  8502  negeu  8518  subadd2  8531  subcan2  8552  addrsub  8698  ltaddneg  8753  ltaddnegr  8754  ltadd1  8758  leadd2  8760  ltsubadd  8761  lesubadd  8763  ltaddsub2  8766  leaddsub2  8768  ltaddpos  8781  lesub2  8786  ltsub2  8788  ltnegcon1  8792  ltnegcon2  8793  lenegcon1  8795  lenegcon2  8796  addge01  8801  addge02  8802  suble0  8805  leaddle0  8806  lesub0  8808  eqord2  8813  sublt0d  8900  recexre  8908  reaplt  8918  reapltxor  8919  reapneg  8927  remulext1  8929  apreim  8933  apcotr  8937  apadd2  8939  addext  8940  apsub1  8972  mulcanap2d  8992  diveqap0  9014  diveqap1  9037  apmul2  9121  ltmul2  9188  lemul2  9189  ltmulgt11  9196  ltmulgt12  9197  gt0div  9202  ge0div  9203  ltmuldiv  9206  ltrec1  9220  lerec2  9221  ledivdiv  9222  ltdiv23  9224  lediv23  9225  suprleubex  9286  creur  9291  creui  9292  nn1suc  9325  nnrecl  9565  fcdmnn0fsuppg  9622  znnsub  9700  zgt0ge1  9707  zltlen  9728  nn0n0n1ge2b  9729  nn0le2is012  9732  btwnnz  9744  gtndiv  9745  prime  9749  eluz2  9936  indstr2  10018  negm  10024  nn01to3  10026  qapne  10048  qltlen  10049  qreccl  10051  irrmulap  10058  divlt1lt  10135  divle1le  10136  nnledivrp  10177  xnn0xadd0  10279  xltadd2  10289  xsubge0  10293  xlesubadd  10295  iccid  10337  elioc2  10348  elico2  10349  elicc2  10350  elfz2  10428  fzen  10457  fzsubel  10476  elfzp1  10489  fzpr  10494  fzrevral2  10523  fzrevral3  10524  nn0disj  10555  2ffzeq  10558  fzosplitsni  10664  fvinim0ffz  10670  ioo0  10704  ico0  10706  ioc0  10707  modq0  10779  negqmod0  10781  zmodidfzo  10803  frecuzrdgtcl  10862  nn0ennn  10883  nninfinf  10893  sq11  11062  nn0le2msqd  11171  nn0opth2d  11175  hashen  11237  zfz1isolem1  11306  zfz1iso  11307  csbwrdg  11348  wrdnval  11349  eqwrd  11359  ccat0  11378  ccatws1lenp1bg  11417  swrd0g  11446  swrdspsleq  11453  pfxeq  11482  pfxsuffeqwrdeq  11484  pfxsuff1eqwrdeq  11485  ccatopth2  11503  wrd2ind  11509  2shfti  11610  cjap  11686  cnreim  11758  rexfiuz  11769  rexanuz2  11771  abs00ap  11842  absext  11843  sqabs  11863  abslt  11869  absle  11870  absdiflt  11873  absdifle  11874  lenegsq  11876  minmax  12011  ltmininf  12016  mingeb  12024  xrminmax  12047  xrmin1inf  12049  xrmin2inf  12050  xrltmininf  12052  xrlemininf  12053  clim  12063  clim0c  12068  climrecvg1n  12130  zsumdc  12167  fsum2dlemstep  12217  binomlem  12266  pwm1geoserap1  12291  zproddc  12362  efieq  12518  sin01bnd  12540  cos01bnd  12541  dvdsval2  12573  modm1div  12583  zdvdsdc  12595  modmulconst  12606  dvdsaddr  12620  dvdsabseq  12630  fzocongeq  12641  zeo3  12651  odd2np1  12656  oddp1d2  12673  zob  12674  oddm1d2  12675  nnoddm1d2  12693  divalgb  12708  divalgmod  12710  modremain  12712  bits0  12731  bitsp1e  12735  bitsp1o  12736  bitscmp  12741  bitsinv1lem  12744  gcdn0gt0  12771  bezoutlemstep  12790  dvdssq  12824  nn0seqcvgd  12835  algcvgblem  12843  lcmdvds  12873  lcmgcdeq  12877  coprmdvds  12886  qredeq  12890  congr  12894  isprm2  12911  isprm3  12912  prmdvdsexp  12943  prmdvdsexpb  12944  prmexpb  12946  prmfac1  12947  cncongrprm  12952  nnmaxpwlemxy  12964  nnmaxpwlemnfac  12967  qnumdenbi  12988  qnumgt0  12994  hashdvds  13019  crth  13022  fermltl  13032  modprminveq  13049  pcpremul  13092  pc2dvds  13129  pcz  13131  prmpwdvds  13154  4sqlem16  13205  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemodife  13289  ballotfilemrv1  13313  ballotfilemrv2  13314  ballotfilem1ri  13327  oddennn  13332  ctinfomlemom  13367  mgm1  13739  ismhm  13817  mhmpropd  13822  issubm  13828  issubm2  13829  grpsubrcan  13935  grplactcnv  13956  grp1  13960  eqgval  14075  eqgid  14078  quselbasg  14082  isghm  14095  conjnmzb  14132  iscmn  14145  eqgabl  14183  prdsbasmpt  14229  prdsbasmpt2  14237  rngmneg1  14295  rngmneg2  14296  rngpropd  14303  rngen1zr  14309  srgen1zr0  14341  ringideu  14370  ringpropd  14392  crngpropd  14393  dvdsrd  14450  dvdsr02  14461  opprunitd  14466  crngunit  14467  unitpropdg  14504  rhmunitinv  14534  isnzr2  14540  issubrng  14556  resrhm2b  14606  aprval  14640  aprunit  14641  isdrngtap  14655  opprdrng  14669  islmod  14676  islssm  14743  islssmg  14744  ellspsn  14803  isridl  14890  zrhrhmb  15006  zndvds  15033  znleval  15037  isassa  15051  istopg  15149  eltg  15202  eltg2  15203  tgss2  15229  bastop1  15233  bastop2  15234  iscld  15253  isnei  15294  neiint  15295  iscn  15347  iscnp  15349  iscnp3  15353  tgcn  15358  ssidcn  15360  lmbr2  15364  lmbrf  15365  cnnei  15382  cnrest2  15386  eltx  15409  imasnopn  15449  ispsmet  15473  ismet  15494  isxmet  15495  metn0  15528  xmetres2  15529  elbl3ps  15544  elbl3  15545  xblpnfps  15548  xblpnf  15549  elmopn2  15599  metss  15644  bdxmet  15651  metrest  15656  xmetxp  15657  xmetxpbl  15658  metcnp3  15661  metcnp  15662  metcnp2  15663  metcn  15664  txmetcnp  15668  txmetcn  15669  metcnpd  15670  bl2ioo  15700  addcncntoplem  15711  elcncf  15723  elcncf2  15724  ivthdec  15794  ellimc3apf  15810  cnlimcim  15821  dveflem  15876  ply1termlem  15892  sincosq2sgn  15978  sinq12gt0  15981  logltb  16026  ltexp2  16096  birthdaylem3  16146  wilthlem1  16151  ppiublem1  16192  prmefexple  16206  bposlem1  16209  lgsdilem  16244  lgsdir2lem4  16248  lgsdir2  16250  lgsne0  16255  lgsabs1  16256  gausslemma2dlem3  16280  gausslemma2dlem7  16285  lgseisenlem3  16289  lgsquad3  16301  2lgslem1a  16305  2lgslem3c  16312  2lgslem3d  16313  2lgsoddprmlem4  16329  2sqlem7  16338  2sqlem8a  16339  uhgreq12g  16415  isuhgropm  16420  uhgr0e  16421  upgrop  16443  uhgrvtxedgiedgb  16482  isuspgropen  16503  isusgropen  16504  uhgr2edg  16545  issubgr2  16597  uhgrspansubgrlem  16615  vtxd0nedgbfi  16638  1loopgrvd0fi  16645  iswlk  16662  upgriswlkdc  16699  istrl  16724  iseupth  16786  eupth2lem2dc  16798  eupth2lem3lem3fi  16809  eupth2lem3lem4fi  16812  eupth2lem3lem7fi  16813  cbvrald  16914  bj-nalset  17019  bj-sels  17038  bj-nnelirr  17077  stnot  17137  isomninnlem  17177  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200