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  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  3629  sbcssg  3633  ralsng  3745  2ralunsn  3919  csbunig  3938  disjeq12d  4110  breq123d  4139  sbcbr12g  4181  sbcbr1g  4182  sbcbr2g  4183  treq  4230  nalset  4258  exmidsssn  4334  copsex4g  4382  onsucb  4645  posng  4842  csbxpg  4851  sbcrel  4856  csbcnvg  4959  eliniseg  5152  brcodir  5170  csbrng  5244  sbcfung  5396  fneq12d  5468  feq12d  5518  feq123d  5519  sbcfng  5526  sbcfg  5527  f1osng  5677  csbfv12g  5730  funimass4  5747  dmfco  5767  eqfnfv  5797  eqfnfv2  5798  fneqeql2  5809  fvimacnvi  5814  funimass3  5816  fniniseg  5820  unpreima  5824  ralrnmpt  5841  rexrnmpt  5842  dffo3  5846  fmptco  5865  fressnfv  5893  eufnfv  5939  foima2  5947  fnunirn  5963  dff13  5964  f1elima  5969  cocan1  5983  cocan2  5984  fliftel  5989  fliftf  5995  isoresbr  6005  isoini  6014  f1oiso  6022  f1ofveu  6063  mpoeq123dva  6139  ovid  6195  ov  6198  ovg  6218  ovelrn  6228  caovord2d  6249  ofrfval2  6309  offveqb  6312  eqop  6401  reldm  6410  f1od2  6461  suppval1  6469  suppssrst  6491  suppssrgst  6492  mpoxopoveq  6501  mpoxopovel  6502  tpostpos  6525  smoiso  6563  frecabcl  6660  frecsuclem  6667  nnaordr  6773  nnaword  6774  nnaordex  6791  ereq1  6804  brdifun  6824  erth2  6844  qliftfun  6881  brecop  6889  elmapg  6925  elpmg  6928  mapsnd  6960  dom2lem  7048  xpcomco  7114  pw2f1odclem  7124  php5fin  7176  funisfsupp  7281  ffsuppbi  7290  elfi2  7296  supisolem  7338  inflbti  7354  inl11  7395  ismkvnex  7485  mkvprop  7488  nninfwlporlemd  7502  exmidfodomrlemreseldju  7542  ltapig  7695  ltmpig  7696  nlt1pig  7698  mulcmpblnq  7725  ltsonq  7755  lt2addnq  7761  lt2mulnq  7762  archnqq  7774  prarloclemarch  7775  ltrnqg  7777  mulcmpblnq0  7801  preqlu  7829  genpdflem  7864  addnqprllem  7884  addnqprulem  7885  addlocprlemgt  7891  appdivnq  7920  mulnqprl  7925  mulnqpru  7926  mullocprlem  7927  distrlem4prl  7941  distrlem4pru  7942  1idprl  7947  1idpru  7948  ltexprlemloc  7964  cauappcvgprlemladdrl  8014  cauappcvgprlemladd  8015  cauappcvgprlem1  8016  archrecnq  8020  caucvgprlemnkj  8023  caucvgprprlemexb  8064  addcmpblnr  8096  lttrsr  8119  ltsosr  8121  ltasrg  8127  mulextsr1  8138  srpospr  8140  caucvgsrlemcau  8150  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  map2psrprg  8162  ltresr  8196  axcaucvglemres  8256  eqlelt  8402  cnegexlem1  8491  negeu  8507  subadd2  8520  subcan2  8541  addrsub  8687  ltaddneg  8742  ltaddnegr  8743  ltadd1  8747  leadd2  8749  ltsubadd  8750  lesubadd  8752  ltaddsub2  8755  leaddsub2  8757  ltaddpos  8770  lesub2  8775  ltsub2  8777  ltnegcon1  8781  ltnegcon2  8782  lenegcon1  8784  lenegcon2  8785  addge01  8790  addge02  8791  suble0  8794  leaddle0  8795  lesub0  8797  eqord2  8802  sublt0d  8888  recexre  8896  reaplt  8906  reapltxor  8907  reapneg  8915  remulext1  8917  apreim  8921  apcotr  8925  apadd2  8927  addext  8928  apsub1  8960  mulcanap2d  8980  diveqap0  9002  diveqap1  9025  apmul2  9109  ltmul2  9176  lemul2  9177  ltmulgt11  9184  ltmulgt12  9185  gt0div  9190  ge0div  9191  ltmuldiv  9194  ltrec1  9208  lerec2  9209  ledivdiv  9210  ltdiv23  9212  lediv23  9213  suprleubex  9274  creur  9279  creui  9280  nn1suc  9302  nnrecl  9540  fcdmnn0fsuppg  9597  znnsub  9675  zgt0ge1  9682  zltlen  9703  nn0n0n1ge2b  9704  nn0le2is012  9707  btwnnz  9719  gtndiv  9720  prime  9724  eluz2  9906  indstr2  9988  negm  9994  nn01to3  9996  qapne  10018  qltlen  10019  qreccl  10021  irrmulap  10027  divlt1lt  10104  divle1le  10105  nnledivrp  10146  xnn0xadd0  10248  xltadd2  10258  xsubge0  10262  xlesubadd  10264  iccid  10306  elioc2  10317  elico2  10318  elicc2  10319  elfz2  10397  fzen  10426  fzsubel  10444  elfzp1  10457  fzpr  10462  fzrevral2  10491  fzrevral3  10492  nn0disj  10523  2ffzeq  10526  fzosplitsni  10632  fvinim0ffz  10638  ioo0  10672  ico0  10674  ioc0  10675  modq0  10744  negqmod0  10746  zmodidfzo  10768  frecuzrdgtcl  10827  nn0ennn  10848  nninfinf  10858  sq11  11027  nn0le2msqd  11135  nn0opth2d  11139  hashen  11201  zfz1isolem1  11270  zfz1iso  11271  csbwrdg  11312  wrdnval  11313  eqwrd  11323  ccat0  11342  ccatws1lenp1bg  11381  swrd0g  11410  swrdspsleq  11417  pfxeq  11446  pfxsuffeqwrdeq  11448  pfxsuff1eqwrdeq  11449  ccatopth2  11467  wrd2ind  11473  2shfti  11574  cjap  11650  cnreim  11722  rexfiuz  11733  rexanuz2  11735  abs00ap  11806  absext  11807  sqabs  11826  abslt  11832  absle  11833  absdiflt  11836  absdifle  11837  lenegsq  11839  minmax  11974  ltmininf  11979  mingeb  11986  xrminmax  12009  xrmin1inf  12011  xrmin2inf  12012  xrltmininf  12014  xrlemininf  12015  clim  12025  clim0c  12030  climrecvg1n  12092  zsumdc  12129  fsum2dlemstep  12179  binomlem  12228  pwm1geoserap1  12253  zproddc  12324  efieq  12480  sin01bnd  12502  cos01bnd  12503  dvdsval2  12535  modm1div  12545  zdvdsdc  12557  modmulconst  12568  dvdsaddr  12582  dvdsabseq  12592  fzocongeq  12603  zeo3  12613  odd2np1  12618  oddp1d2  12635  zob  12636  oddm1d2  12637  nnoddm1d2  12655  divalgb  12670  divalgmod  12672  modremain  12674  bits0  12693  bitsp1e  12697  bitsp1o  12698  bitscmp  12703  bitsinv1lem  12706  gcdn0gt0  12733  bezoutlemstep  12752  dvdssq  12786  nn0seqcvgd  12797  algcvgblem  12805  lcmdvds  12835  lcmgcdeq  12839  coprmdvds  12848  qredeq  12852  congr  12856  isprm2  12873  isprm3  12874  prmdvdsexp  12904  prmdvdsexpb  12905  prmexpb  12907  prmfac1  12908  cncongrprm  12913  oddpwdclemxy  12925  oddpwdclemodd  12928  qnumdenbi  12948  qnumgt0  12954  hashdvds  12977  crth  12980  fermltl  12990  modprminveq  13007  pcpremul  13050  pc2dvds  13087  pcz  13089  prmpwdvds  13112  4sqlem16  13163  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemodife  13218  ballotfilemrv1  13242  ballotfilemrv2  13243  ballotfilem1ri  13256  oddennn  13261  ctinfomlemom  13296  mgm1  13667  ismhm  13745  mhmpropd  13750  issubm  13756  issubm2  13757  grpsubrcan  13863  grplactcnv  13884  grp1  13888  eqgval  14003  eqgid  14006  quselbasg  14010  isghm  14023  conjnmzb  14060  iscmn  14073  eqgabl  14111  prdsbasmpt  14157  prdsbasmpt2  14165  rngmneg1  14221  rngmneg2  14222  rngpropd  14229  rngen1zr  14235  srgen1zr0  14266  ringideu  14295  ringpropd  14316  crngpropd  14317  dvdsrd  14374  dvdsr02  14385  opprunitd  14390  crngunit  14391  unitpropdg  14428  rhmunitinv  14458  isnzr2  14464  issubrng  14480  resrhm2b  14530  aprval  14564  aprunit  14565  isdrngtap  14579  opprdrng  14593  islmod  14600  islssm  14666  islssmg  14667  ellspsn  14726  isridl  14813  zrhrhmb  14929  zndvds  14956  znleval  14960  istopg  15023  eltg  15076  eltg2  15077  tgss2  15103  bastop1  15107  bastop2  15108  iscld  15127  isnei  15168  neiint  15169  iscn  15221  iscnp  15223  iscnp3  15227  tgcn  15232  ssidcn  15234  lmbr2  15238  lmbrf  15239  cnnei  15256  cnrest2  15260  eltx  15283  imasnopn  15323  ispsmet  15347  ismet  15368  isxmet  15369  metn0  15402  xmetres2  15403  elbl3ps  15418  elbl3  15419  xblpnfps  15422  xblpnf  15423  elmopn2  15473  metss  15518  bdxmet  15525  metrest  15530  xmetxp  15531  xmetxpbl  15532  metcnp3  15535  metcnp  15536  metcnp2  15537  metcn  15538  txmetcnp  15542  txmetcn  15543  metcnpd  15544  bl2ioo  15574  addcncntoplem  15585  elcncf  15597  elcncf2  15598  ivthdec  15668  ellimc3apf  15684  cnlimcim  15695  dveflem  15750  ply1termlem  15766  sincosq2sgn  15851  sinq12gt0  15854  logltb  15898  ltexp2  15966  wilthlem1  16008  lgsdilem  16060  lgsdir2lem4  16064  lgsdir2  16066  lgsne0  16071  lgsabs1  16072  gausslemma2dlem3  16096  gausslemma2dlem7  16101  lgseisenlem3  16105  lgsquad3  16117  2lgslem1a  16121  2lgslem3c  16128  2lgslem3d  16129  2lgsoddprmlem4  16145  2sqlem7  16154  2sqlem8a  16155  uhgreq12g  16231  isuhgropm  16236  uhgr0e  16237  upgrop  16259  uhgrvtxedgiedgb  16298  isuspgropen  16319  isusgropen  16320  uhgr2edg  16361  issubgr2  16413  uhgrspansubgrlem  16431  vtxd0nedgbfi  16454  1loopgrvd0fi  16461  iswlk  16478  upgriswlkdc  16515  istrl  16540  iseupth  16602  eupth2lem2dc  16614  eupth2lem3lem3fi  16625  eupth2lem3lem4fi  16628  eupth2lem3lem7fi  16629  cbvrald  16730  bj-nalset  16835  bj-sels  16854  bj-nnelirr  16893  isomninnlem  16984  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007