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  793  con1biidc  877  pm4.54dc  902  dn1dc  960  dedlem0a  968  xorbi12d  1382  nbbndc  1394  eleq12d  2248  neeq12d  2367  neleq12d  2448  raleqbi1dv  2680  rexeqbi1dv  2681  reueqd  2682  rmoeqd  2683  raleqbidv  2684  rexeqbidv  2685  raleqbidva  2686  rexeqbidva  2687  eueq3dc  2911  sbc19.21g  3031  sbcabel  3044  sbcel1g  3076  sbceq1g  3077  sbcel2g  3078  sbceq2g  3079  sbccsb2g  3087  sbcco3g  3114  sseq12d  3186  raaanlem  3528  sbcssg  3532  ralsng  3632  2ralunsn  3798  csbunig  3817  disjeq12d  3989  breq123d  4017  sbcbr12g  4058  sbcbr1g  4059  sbcbr2g  4060  treq  4107  nalset  4133  exmidsssn  4202  copsex4g  4247  onsucb  4502  posng  4698  csbxpg  4707  sbcrel  4712  csbcnvg  4811  eliniseg  4998  brcodir  5016  csbrng  5090  sbcfung  5240  fneq12d  5308  feq12d  5355  feq123d  5356  sbcfng  5363  sbcfg  5364  f1osng  5502  csbfv12g  5551  funimass4  5566  dmfco  5584  eqfnfv  5613  eqfnfv2  5614  fneqeql2  5625  fvimacnvi  5630  funimass3  5632  fniniseg  5636  rexsupp  5640  unpreima  5641  ralrnmpt  5658  rexrnmpt  5659  dffo3  5663  fmptco  5682  fressnfv  5703  eufnfv  5747  foima2  5752  fnunirn  5767  dff13  5768  f1elima  5773  cocan1  5787  cocan2  5788  fliftel  5793  fliftf  5799  isoresbr  5809  isoini  5818  f1oiso  5826  f1ofveu  5862  mpoeq123dva  5935  ovid  5990  ov  5993  ovg  6012  ovelrn  6022  caovord2d  6043  ofrfval2  6098  offveqb  6101  eqop  6177  reldm  6186  f1od2  6235  mpoxopoveq  6240  mpoxopovel  6241  tpostpos  6264  smoiso  6302  frecabcl  6399  frecsuclem  6406  nnaordr  6510  nnaword  6511  nnaordex  6528  ereq1  6541  brdifun  6561  erth2  6579  qliftfun  6616  brecop  6624  elmapg  6660  elpmg  6663  dom2lem  6771  xpcomco  6825  php5fin  6881  elfi2  6970  supisolem  7006  inflbti  7022  inl11  7063  ismkvnex  7152  mkvprop  7155  nninfwlporlemd  7169  exmidfodomrlemreseldju  7198  ltapig  7336  ltmpig  7337  nlt1pig  7339  mulcmpblnq  7366  ltsonq  7396  lt2addnq  7402  lt2mulnq  7403  archnqq  7415  prarloclemarch  7416  ltrnqg  7418  mulcmpblnq0  7442  preqlu  7470  genpdflem  7505  addnqprllem  7525  addnqprulem  7526  addlocprlemgt  7532  appdivnq  7561  mulnqprl  7566  mulnqpru  7567  mullocprlem  7568  distrlem4prl  7582  distrlem4pru  7583  1idprl  7588  1idpru  7589  ltexprlemloc  7605  cauappcvgprlemladdrl  7655  cauappcvgprlemladd  7656  cauappcvgprlem1  7657  archrecnq  7661  caucvgprlemnkj  7664  caucvgprprlemexb  7705  addcmpblnr  7737  lttrsr  7760  ltsosr  7762  ltasrg  7768  mulextsr1  7779  srpospr  7781  caucvgsrlemcau  7791  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  map2psrprg  7803  ltresr  7837  axcaucvglemres  7897  eqlelt  8043  cnegexlem1  8131  negeu  8147  subadd2  8160  subcan2  8181  addrsub  8327  ltaddneg  8380  ltaddnegr  8381  ltadd1  8385  leadd2  8387  ltsubadd  8388  lesubadd  8390  ltaddsub2  8393  leaddsub2  8395  ltaddpos  8408  lesub2  8413  ltsub2  8415  ltnegcon1  8419  ltnegcon2  8420  lenegcon1  8422  lenegcon2  8423  addge01  8428  addge02  8429  suble0  8432  leaddle0  8433  lesub0  8435  eqord2  8440  sublt0d  8526  recexre  8534  reaplt  8544  reapltxor  8545  reapneg  8553  remulext1  8555  apreim  8559  apcotr  8563  apadd2  8565  addext  8566  apsub1  8598  mulcanap2d  8618  diveqap0  8638  diveqap1  8661  apmul2  8745  ltmul2  8812  lemul2  8813  ltmulgt11  8820  ltmulgt12  8821  gt0div  8826  ge0div  8827  ltmuldiv  8830  ltrec1  8844  lerec2  8845  ledivdiv  8846  ltdiv23  8848  lediv23  8849  suprleubex  8910  creur  8915  creui  8916  nn1suc  8937  nnrecl  9173  znnsub  9303  zgt0ge1  9310  zltlen  9330  nn0n0n1ge2b  9331  nn0le2is012  9334  btwnnz  9346  gtndiv  9347  prime  9351  eluz2  9533  indstr2  9608  negm  9614  nn01to3  9616  qapne  9638  qltlen  9639  qreccl  9641  divlt1lt  9723  divle1le  9724  nnledivrp  9765  xnn0xadd0  9866  xltadd2  9876  xsubge0  9880  xlesubadd  9882  iccid  9924  elioc2  9935  elico2  9936  elicc2  9937  elfz2  10014  fzen  10042  fzsubel  10059  elfzp1  10071  fzpr  10076  fzrevral2  10105  fzrevral3  10106  nn0disj  10137  2ffzeq  10140  fzosplitsni  10234  fvinim0ffz  10240  ioo0  10259  ico0  10261  ioc0  10262  modq0  10328  negqmod0  10330  zmodidfzo  10352  frecuzrdgtcl  10411  nn0ennn  10432  sq11  10592  nn0le2msqd  10698  nn0opth2d  10702  hashen  10763  zfz1isolem1  10819  zfz1iso  10820  2shfti  10839  cjap  10914  cnreim  10986  rexfiuz  10997  rexanuz2  10999  abs00ap  11070  absext  11071  sqabs  11090  abslt  11096  absle  11097  absdiflt  11100  absdifle  11101  lenegsq  11103  minmax  11237  ltmininf  11242  mingeb  11249  xrminmax  11272  xrmin1inf  11274  xrmin2inf  11275  xrltmininf  11277  xrlemininf  11278  clim  11288  clim0c  11293  climrecvg1n  11355  zsumdc  11391  fsum2dlemstep  11441  binomlem  11490  pwm1geoserap1  11515  zproddc  11586  efieq  11742  sin01bnd  11764  cos01bnd  11765  dvdsval2  11796  modm1div  11806  zdvdsdc  11818  modmulconst  11829  dvdsaddr  11843  dvdsabseq  11852  fzocongeq  11863  zeo3  11872  odd2np1  11877  oddp1d2  11894  zob  11895  oddm1d2  11896  nnoddm1d2  11914  divalgb  11929  divalgmod  11931  modremain  11933  gcdn0gt0  11978  bezoutlemstep  11997  dvdssq  12031  nn0seqcvgd  12040  algcvgblem  12048  lcmdvds  12078  lcmgcdeq  12082  coprmdvds  12091  qredeq  12095  congr  12099  isprm2  12116  isprm3  12117  prmdvdsexp  12147  prmdvdsexpb  12148  prmexpb  12150  prmfac1  12151  cncongrprm  12156  oddpwdclemxy  12168  oddpwdclemodd  12171  qnumdenbi  12191  qnumgt0  12197  hashdvds  12220  crth  12223  fermltl  12233  modprminveq  12249  pcpremul  12292  pc2dvds  12328  pcz  12330  prmpwdvds  12352  oddennn  12392  ctinfomlemom  12427  mgm1  12788  ismhm  12852  mhmpropd  12856  issubm  12862  issubm2  12863  grpsubrcan  12950  grplactcnv  12971  grp1  12975  eqgval  13080  eqgid  13083  iscmn  13094  srgen1zr  13169  ringideu  13198  ringpropd  13215  crngpropd  13216  dvdsrd  13261  dvdsr02  13272  opprunitd  13277  crngunit  13278  unitpropdg  13315  aprval  13370  islmod  13379  istopg  13469  eltg  13522  eltg2  13523  tgss2  13549  bastop1  13553  bastop2  13554  iscld  13573  isnei  13614  neiint  13615  iscn  13667  iscnp  13669  iscnp3  13673  tgcn  13678  ssidcn  13680  lmbr2  13684  lmbrf  13685  cnnei  13702  cnrest2  13706  eltx  13729  imasnopn  13769  ispsmet  13793  ismet  13814  isxmet  13815  metn0  13848  xmetres2  13849  elbl3ps  13864  elbl3  13865  xblpnfps  13868  xblpnf  13869  elmopn2  13919  metss  13964  bdxmet  13971  metrest  13976  xmetxp  13977  xmetxpbl  13978  metcnp3  13981  metcnp  13982  metcnp2  13983  metcn  13984  txmetcnp  13988  txmetcn  13989  metcnpd  13990  bl2ioo  14012  addcncntoplem  14021  elcncf  14030  elcncf2  14031  ivthdec  14092  ellimc3apf  14099  cnlimcim  14110  dveflem  14157  sincosq2sgn  14218  sinq12gt0  14221  logltb  14265  ltexp2  14330  lgsdilem  14398  lgsdir2lem4  14402  lgsdir2  14404  lgsne0  14409  lgsabs1  14410  2lgsoddprmlem4  14430  2sqlem7  14438  2sqlem8a  14439  cbvrald  14510  bj-nalset  14617  bj-sels  14636  bj-nnelirr  14675  isomninnlem  14748  iswomninnlem  14767  iswomni0  14769  ismkvnnlem  14770