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  7349  inflbti  7365  inl11  7406  ismkvnex  7496  mkvprop  7499  nninfwlporlemd  7513  exmidfodomrlemreseldju  7553  ltapig  7706  ltmpig  7707  nlt1pig  7709  mulcmpblnq  7736  ltsonq  7766  lt2addnq  7772  lt2mulnq  7773  archnqq  7785  prarloclemarch  7786  ltrnqg  7788  mulcmpblnq0  7812  preqlu  7840  genpdflem  7875  addnqprllem  7895  addnqprulem  7896  addlocprlemgt  7902  appdivnq  7931  mulnqprl  7936  mulnqpru  7937  mullocprlem  7938  distrlem4prl  7952  distrlem4pru  7953  1idprl  7958  1idpru  7959  ltexprlemloc  7975  cauappcvgprlemladdrl  8025  cauappcvgprlemladd  8026  cauappcvgprlem1  8027  archrecnq  8031  caucvgprlemnkj  8034  caucvgprprlemexb  8075  addcmpblnr  8107  lttrsr  8130  ltsosr  8132  ltasrg  8138  mulextsr1  8149  srpospr  8151  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  map2psrprg  8173  ltresr  8207  axcaucvglemres  8267  eqlelt  8413  cnegexlem1  8503  negeu  8519  subadd2  8532  subcan2  8553  addrsub  8699  ltaddneg  8754  ltaddnegr  8755  ltadd1  8759  leadd2  8761  ltsubadd  8762  lesubadd  8764  ltaddsub2  8767  leaddsub2  8769  ltaddpos  8782  lesub2  8787  ltsub2  8789  ltnegcon1  8793  ltnegcon2  8794  lenegcon1  8796  lenegcon2  8797  addge01  8802  addge02  8803  suble0  8806  leaddle0  8807  lesub0  8809  eqord2  8814  sublt0d  8901  recexre  8909  reaplt  8919  reapltxor  8920  reapneg  8928  remulext1  8930  apreim  8934  apcotr  8938  apadd2  8940  addext  8941  apsub1  8973  mulcanap2d  8993  diveqap0  9015  diveqap1  9038  apmul2  9122  ltmul2  9189  lemul2  9190  ltmulgt11  9197  ltmulgt12  9198  gt0div  9203  ge0div  9204  ltmuldiv  9207  ltrec1  9221  lerec2  9222  ledivdiv  9223  ltdiv23  9225  lediv23  9226  suprleubex  9287  creur  9292  creui  9293  nn1suc  9326  nnrecl  9566  fcdmnn0fsuppg  9623  znnsub  9701  zgt0ge1  9708  zltlen  9729  nn0n0n1ge2b  9730  nn0le2is012  9733  btwnnz  9745  gtndiv  9746  prime  9750  eluz2  9937  indstr2  10019  negm  10025  nn01to3  10027  qapne  10049  qltlen  10050  qreccl  10052  irrmulap  10059  divlt1lt  10136  divle1le  10137  nnledivrp  10178  xnn0xadd0  10280  xltadd2  10290  xsubge0  10294  xlesubadd  10296  iccid  10338  elioc2  10349  elico2  10350  elicc2  10351  elfz2  10429  fzen  10458  fzsubel  10477  elfzp1  10490  fzpr  10495  fzrevral2  10524  fzrevral3  10525  nn0disj  10556  2ffzeq  10559  fzosplitsni  10665  fvinim0ffz  10671  ioo0  10705  ico0  10707  ioc0  10708  modq0  10781  negqmod0  10783  zmodidfzo  10805  frecuzrdgtcl  10864  nn0ennn  10885  nninfinf  10895  sq11  11064  nn0le2msqd  11173  nn0opth2d  11177  hashen  11239  zfz1isolem1  11308  zfz1iso  11309  csbwrdg  11350  wrdnval  11351  eqwrd  11361  ccat0  11380  ccatws1lenp1bg  11419  swrd0g  11448  swrdspsleq  11455  pfxeq  11484  pfxsuffeqwrdeq  11486  pfxsuff1eqwrdeq  11487  ccatopth2  11505  wrd2ind  11511  2shfti  11612  cjap  11688  cnreim  11760  rexfiuz  11771  rexanuz2  11773  abs00ap  11844  absext  11845  sqabs  11865  abslt  11871  absle  11872  absdiflt  11875  absdifle  11876  lenegsq  11878  minmax  12014  ltmininf  12019  mingeb  12027  xrminmax  12050  xrmin1inf  12052  xrmin2inf  12053  xrltmininf  12055  xrlemininf  12056  clim  12066  clim0c  12071  climrecvg1n  12133  zsumdc  12170  fsum2dlemstep  12220  binomlem  12269  pwm1geoserap1  12294  zproddc  12365  efieq  12521  sin01bnd  12543  cos01bnd  12544  dvdsval2  12576  modm1div  12586  zdvdsdc  12598  modmulconst  12609  dvdsaddr  12623  dvdsabseq  12633  fzocongeq  12644  zeo3  12654  odd2np1  12659  oddp1d2  12676  zob  12677  oddm1d2  12678  nnoddm1d2  12696  divalgb  12711  divalgmod  12713  modremain  12715  bits0  12734  bitsp1e  12738  bitsp1o  12739  bitscmp  12744  bitsinv1lem  12747  gcdn0gt0  12774  bezoutlemstep  12793  dvdssq  12827  nn0seqcvgd  12838  algcvgblem  12846  lcmdvds  12876  lcmgcdeq  12880  coprmdvds  12889  qredeq  12893  congr  12897  isprm2  12914  isprm3  12915  prmdvdsexp  12946  prmdvdsexpb  12947  prmexpb  12949  prmfac1  12950  cncongrprm  12955  nnmaxpwlemxy  12967  nnmaxpwlemnfac  12970  qnumdenbi  12991  qnumgt0  12997  hashdvds  13022  crth  13025  fermltl  13035  modprminveq  13052  pcpremul  13095  pc2dvds  13132  pcz  13134  prmpwdvds  13157  4sqlem16  13208  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemodife  13292  ballotfilemrv1  13316  ballotfilemrv2  13317  ballotfilem1ri  13330  oddennn  13335  ctinfomlemom  13370  mgm1  13743  ismhm  13821  mhmpropd  13826  issubm  13832  issubm2  13833  grpsubrcan  13939  grplactcnv  13960  grp1  13964  eqgval  14079  eqgid  14082  quselbasg  14086  isghm  14099  conjnmzb  14136  iscmn  14180  eqgabl  14218  prdsbasmpt  14264  prdsbasmpt2  14272  rngmneg1  14330  rngmneg2  14331  rngpropd  14338  rngen1zr  14344  srgen1zr0  14376  ringideu  14405  ringpropd  14427  crngpropd  14428  dvdsrd  14485  dvdsr02  14496  opprunitd  14501  crngunit  14502  unitpropdg  14539  rhmunitinv  14569  isnzr2  14575  issubrng  14591  resrhm2b  14641  aprval  14675  aprunit  14676  isdrngtap  14690  opprdrng  14704  islmod  14711  islssm  14778  islssmg  14779  ellspsn  14838  isridl  14925  zrhrhmb  15041  zndvds  15068  znleval  15072  isassa  15086  istopg  15191  eltg  15244  eltg2  15245  tgss2  15271  bastop1  15275  bastop2  15276  iscld  15295  isnei  15336  neiint  15337  iscn  15389  iscnp  15391  iscnp3  15395  tgcn  15400  ssidcn  15402  lmbr2  15406  lmbrf  15407  cnnei  15424  cnrest2  15428  eltx  15451  imasnopn  15491  ispsmet  15515  ismet  15536  isxmet  15537  metn0  15570  xmetres2  15571  elbl3ps  15586  elbl3  15587  xblpnfps  15590  xblpnf  15591  elmopn2  15641  metss  15686  bdxmet  15693  metrest  15698  xmetxp  15699  xmetxpbl  15700  metcnp3  15703  metcnp  15704  metcnp2  15705  metcn  15706  txmetcnp  15710  txmetcn  15711  metcnpd  15712  bl2ioo  15742  addcncntoplem  15753  elcncf  15765  elcncf2  15766  ivthdec  15836  ellimc3apf  15852  cnlimcim  15863  dveflem  15918  ply1termlem  15934  sincosq2sgn  16020  sinq12gt0  16023  logltb  16068  ltexp2  16138  birthdaylem3  16188  wilthlem1  16193  ppiublem1  16252  prmefexple  16269  bposlem1  16272  bposlem6  16277  bposlem7  16278  lgsdilem  16312  lgsdir2lem4  16316  lgsdir2  16318  lgsne0  16323  lgsabs1  16324  gausslemma2dlem3  16348  gausslemma2dlem7  16353  lgseisenlem3  16357  lgsquad3  16369  2lgslem1a  16373  2lgslem3c  16380  2lgslem3d  16381  2lgsoddprmlem4  16397  2sqlem7  16406  2sqlem8a  16407  uhgreq12g  16483  isuhgropm  16488  uhgr0e  16489  upgrop  16511  uhgrvtxedgiedgb  16550  isuspgropen  16571  isusgropen  16572  uhgr2edg  16613  issubgr2  16665  uhgrspansubgrlem  16683  vtxd0nedgbfi  16706  1loopgrvd0fi  16713  iswlk  16730  upgriswlkdc  16767  istrl  16792  iseupth  16854  eupth2lem2dc  16866  eupth2lem3lem3fi  16877  eupth2lem3lem4fi  16880  eupth2lem3lem7fi  16881  cbvrald  16982  bj-nalset  17087  bj-sels  17106  bj-nnelirr  17145  stnot  17205  isomninnlem  17245  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269