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  800  con1biidc  884  pm4.54dc  909  dn1dc  968  dedlem0a  976  dfifp3dc  990  dfifp4dc  991  dfifp5dc  992  3bior2fd  1390  xorbi12d  1426  nbbndc  1438  eleq12d  2302  neeq12d  2422  neleq12d  2503  raleqbi1dv  2742  rexeqbi1dv  2743  reueqd  2744  rmoeqd  2745  raleqbidv  2746  rexeqbidv  2747  raleqbidva  2748  rexeqbidva  2749  eueq3dc  2980  sbc19.21g  3100  sbcabel  3114  sbcel1g  3146  sbceq1g  3147  sbcel2g  3148  sbceq2g  3149  sbccsb2g  3157  sbcco3g  3185  sseq12d  3258  raaanlem  3599  sbcssg  3603  ralsng  3709  2ralunsn  3882  csbunig  3901  disjeq12d  4073  breq123d  4102  sbcbr12g  4144  sbcbr1g  4145  sbcbr2g  4146  treq  4193  nalset  4219  exmidsssn  4292  copsex4g  4339  onsucb  4601  posng  4798  csbxpg  4807  sbcrel  4812  csbcnvg  4914  eliniseg  5106  brcodir  5124  csbrng  5198  sbcfung  5350  fneq12d  5422  feq12d  5472  feq123d  5473  sbcfng  5480  sbcfg  5481  f1osng  5626  csbfv12g  5679  funimass4  5696  dmfco  5714  eqfnfv  5744  eqfnfv2  5745  fneqeql2  5756  fvimacnvi  5761  funimass3  5763  fniniseg  5767  rexsupp  5771  unpreima  5772  ralrnmpt  5789  rexrnmpt  5790  dffo3  5794  fmptco  5813  fressnfv  5840  eufnfv  5884  foima2  5891  fnunirn  5907  dff13  5908  f1elima  5913  cocan1  5927  cocan2  5928  fliftel  5933  fliftf  5939  isoresbr  5949  isoini  5958  f1oiso  5966  f1ofveu  6005  mpoeq123dva  6081  ovid  6137  ov  6140  ovg  6160  ovelrn  6170  caovord2d  6191  ofrfval2  6251  offveqb  6254  eqop  6339  reldm  6348  f1od2  6399  mpoxopoveq  6405  mpoxopovel  6406  tpostpos  6429  smoiso  6467  frecabcl  6564  frecsuclem  6571  nnaordr  6677  nnaword  6678  nnaordex  6695  ereq1  6708  brdifun  6728  erth2  6748  qliftfun  6785  brecop  6793  elmapg  6829  elpmg  6832  dom2lem  6944  xpcomco  7009  pw2f1odclem  7019  php5fin  7070  elfi2  7170  supisolem  7206  inflbti  7222  inl11  7263  ismkvnex  7353  mkvprop  7356  nninfwlporlemd  7370  exmidfodomrlemreseldju  7410  ltapig  7557  ltmpig  7558  nlt1pig  7560  mulcmpblnq  7587  ltsonq  7617  lt2addnq  7623  lt2mulnq  7624  archnqq  7636  prarloclemarch  7637  ltrnqg  7639  mulcmpblnq0  7663  preqlu  7691  genpdflem  7726  addnqprllem  7746  addnqprulem  7747  addlocprlemgt  7753  appdivnq  7782  mulnqprl  7787  mulnqpru  7788  mullocprlem  7789  distrlem4prl  7803  distrlem4pru  7804  1idprl  7809  1idpru  7810  ltexprlemloc  7826  cauappcvgprlemladdrl  7876  cauappcvgprlemladd  7877  cauappcvgprlem1  7878  archrecnq  7882  caucvgprlemnkj  7885  caucvgprprlemexb  7926  addcmpblnr  7958  lttrsr  7981  ltsosr  7983  ltasrg  7989  mulextsr1  8000  srpospr  8002  caucvgsrlemcau  8012  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  map2psrprg  8024  ltresr  8058  axcaucvglemres  8118  eqlelt  8265  cnegexlem1  8353  negeu  8369  subadd2  8382  subcan2  8403  addrsub  8549  ltaddneg  8603  ltaddnegr  8604  ltadd1  8608  leadd2  8610  ltsubadd  8611  lesubadd  8613  ltaddsub2  8616  leaddsub2  8618  ltaddpos  8631  lesub2  8636  ltsub2  8638  ltnegcon1  8642  ltnegcon2  8643  lenegcon1  8645  lenegcon2  8646  addge01  8651  addge02  8652  suble0  8655  leaddle0  8656  lesub0  8658  eqord2  8663  sublt0d  8749  recexre  8757  reaplt  8767  reapltxor  8768  reapneg  8776  remulext1  8778  apreim  8782  apcotr  8786  apadd2  8788  addext  8789  apsub1  8821  mulcanap2d  8841  diveqap0  8861  diveqap1  8884  apmul2  8968  ltmul2  9035  lemul2  9036  ltmulgt11  9043  ltmulgt12  9044  gt0div  9049  ge0div  9050  ltmuldiv  9053  ltrec1  9067  lerec2  9068  ledivdiv  9069  ltdiv23  9071  lediv23  9072  suprleubex  9133  creur  9138  creui  9139  nn1suc  9161  nnrecl  9399  znnsub  9530  zgt0ge1  9537  zltlen  9557  nn0n0n1ge2b  9558  nn0le2is012  9561  btwnnz  9573  gtndiv  9574  prime  9578  eluz2  9760  indstr2  9842  negm  9848  nn01to3  9850  qapne  9872  qltlen  9873  qreccl  9875  irrmulap  9881  divlt1lt  9958  divle1le  9959  nnledivrp  10000  xnn0xadd0  10101  xltadd2  10111  xsubge0  10115  xlesubadd  10117  iccid  10159  elioc2  10170  elico2  10171  elicc2  10172  elfz2  10249  fzen  10277  fzsubel  10294  elfzp1  10306  fzpr  10311  fzrevral2  10340  fzrevral3  10341  nn0disj  10372  2ffzeq  10375  fzosplitsni  10480  fvinim0ffz  10486  ioo0  10518  ico0  10520  ioc0  10521  modq0  10590  negqmod0  10592  zmodidfzo  10614  frecuzrdgtcl  10673  nn0ennn  10694  nninfinf  10704  sq11  10873  nn0le2msqd  10980  nn0opth2d  10984  hashen  11045  zfz1isolem1  11103  zfz1iso  11104  csbwrdg  11142  wrdnval  11143  eqwrd  11153  ccat0  11172  ccatws1lenp1bg  11211  swrd0g  11240  swrdspsleq  11247  pfxeq  11276  pfxsuffeqwrdeq  11278  pfxsuff1eqwrdeq  11279  ccatopth2  11297  wrd2ind  11303  2shfti  11391  cjap  11466  cnreim  11538  rexfiuz  11549  rexanuz2  11551  abs00ap  11622  absext  11623  sqabs  11642  abslt  11648  absle  11649  absdiflt  11652  absdifle  11653  lenegsq  11655  minmax  11790  ltmininf  11795  mingeb  11802  xrminmax  11825  xrmin1inf  11827  xrmin2inf  11828  xrltmininf  11830  xrlemininf  11831  clim  11841  clim0c  11846  climrecvg1n  11908  zsumdc  11944  fsum2dlemstep  11994  binomlem  12043  pwm1geoserap1  12068  zproddc  12139  efieq  12295  sin01bnd  12317  cos01bnd  12318  dvdsval2  12350  modm1div  12360  zdvdsdc  12372  modmulconst  12383  dvdsaddr  12397  dvdsabseq  12407  fzocongeq  12418  zeo3  12428  odd2np1  12433  oddp1d2  12450  zob  12451  oddm1d2  12452  nnoddm1d2  12470  divalgb  12485  divalgmod  12487  modremain  12489  bits0  12508  bitsp1e  12512  bitsp1o  12513  bitscmp  12518  bitsinv1lem  12521  gcdn0gt0  12548  bezoutlemstep  12567  dvdssq  12601  nn0seqcvgd  12612  algcvgblem  12620  lcmdvds  12650  lcmgcdeq  12654  coprmdvds  12663  qredeq  12667  congr  12671  isprm2  12688  isprm3  12689  prmdvdsexp  12719  prmdvdsexpb  12720  prmexpb  12722  prmfac1  12723  cncongrprm  12728  oddpwdclemxy  12740  oddpwdclemodd  12743  qnumdenbi  12763  qnumgt0  12769  hashdvds  12792  crth  12795  fermltl  12805  modprminveq  12822  pcpremul  12865  pc2dvds  12902  pcz  12904  prmpwdvds  12927  4sqlem16  12978  oddennn  13012  ctinfomlemom  13047  prdsbasmpt  13362  prdsbasmpt2  13370  mgm1  13452  ismhm  13543  mhmpropd  13548  issubm  13554  issubm2  13555  grpsubrcan  13663  grplactcnv  13684  grp1  13688  eqgval  13809  eqgid  13812  quselbasg  13816  isghm  13829  conjnmzb  13866  iscmn  13879  eqgabl  13916  rngmneg1  13959  rngmneg2  13960  rngpropd  13967  srgen1zr  14000  ringideu  14029  ringpropd  14050  crngpropd  14051  dvdsrd  14107  dvdsr02  14118  opprunitd  14123  crngunit  14124  unitpropdg  14161  rhmunitinv  14191  isnzr2  14197  issubrng  14212  resrhm2b  14262  aprval  14295  islmod  14304  islssm  14370  islssmg  14371  ellspsn  14430  isridl  14517  zrhrhmb  14635  zndvds  14662  znleval  14666  istopg  14722  eltg  14775  eltg2  14776  tgss2  14802  bastop1  14806  bastop2  14807  iscld  14826  isnei  14867  neiint  14868  iscn  14920  iscnp  14922  iscnp3  14926  tgcn  14931  ssidcn  14933  lmbr2  14937  lmbrf  14938  cnnei  14955  cnrest2  14959  eltx  14982  imasnopn  15022  ispsmet  15046  ismet  15067  isxmet  15068  metn0  15101  xmetres2  15102  elbl3ps  15117  elbl3  15118  xblpnfps  15121  xblpnf  15122  elmopn2  15172  metss  15217  bdxmet  15224  metrest  15229  xmetxp  15230  xmetxpbl  15231  metcnp3  15234  metcnp  15235  metcnp2  15236  metcn  15237  txmetcnp  15241  txmetcn  15242  metcnpd  15243  bl2ioo  15273  addcncntoplem  15284  elcncf  15296  elcncf2  15297  ivthdec  15367  ellimc3apf  15383  cnlimcim  15394  dveflem  15449  ply1termlem  15465  sincosq2sgn  15550  sinq12gt0  15553  logltb  15597  ltexp2  15664  wilthlem1  15703  lgsdilem  15755  lgsdir2lem4  15759  lgsdir2  15761  lgsne0  15766  lgsabs1  15767  gausslemma2dlem3  15791  gausslemma2dlem7  15796  lgseisenlem3  15800  lgsquad3  15812  2lgslem1a  15816  2lgslem3c  15823  2lgslem3d  15824  2lgsoddprmlem4  15840  2sqlem7  15849  2sqlem8a  15850  uhgreq12g  15926  isuhgropm  15931  uhgr0e  15932  upgrop  15954  uhgrvtxedgiedgb  15993  isuspgropen  16014  isusgropen  16015  uhgr2edg  16056  issubgr2  16108  uhgrspansubgrlem  16126  vtxd0nedgbfi  16149  1loopgrvd0fi  16156  iswlk  16173  upgriswlkdc  16210  istrl  16235  iseupth  16297  eupth2lem2dc  16309  cbvrald  16384  bj-nalset  16490  bj-sels  16509  bj-nnelirr  16548  isomninnlem  16634  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656