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  4145  sbcbr12g  4187  sbcbr1g  4188  sbcbr2g  4189  treq  4237  nalset  4265  exmidsssn  4341  copsex4g  4389  onsucb  4652  posng  4849  csbxpg  4858  sbcrel  4863  csbcnvg  4966  eliniseg  5160  brcodir  5178  csbrng  5252  sbcfung  5404  fneq12d  5476  feq12d  5526  feq123d  5527  sbcfng  5534  sbcfg  5535  f1osng  5685  csbfv12g  5739  funimass4  5756  dmfco  5776  eqfnfv  5809  eqfnfv2  5810  fneqeql2  5821  fvimacnvi  5826  funimass3  5828  fniniseg  5832  unpreima  5836  ralrnmpt  5853  rexrnmpt  5854  dffo3  5858  fmptco  5877  fressnfv  5905  eufnfv  5952  foima2  5960  fnunirn  5976  dff13  5977  f1elima  5982  cocan1  5996  cocan2  5997  fliftel  6002  fliftf  6008  isoresbr  6018  isoini  6027  f1oiso  6035  f1ofveu  6076  mpoeq123dva  6152  ovid  6208  ov  6211  ovg  6231  ovelrn  6241  caovord2d  6262  ofrfval2  6323  offveqb  6326  eqop  6415  reldm  6424  f1od2  6475  suppval1  6483  suppssrst  6505  suppssrgst  6506  mpoxopoveq  6516  mpoxopovel  6517  tpostpos  6540  smoiso  6578  frecabcl  6675  frecsuclem  6682  nnaordr  6788  nnaword  6789  nnaordex  6806  ereq1  6819  brdifun  6839  erth2  6859  qliftfun  6896  brecop  6904  elmapg  6940  elpmg  6943  mapsnd  6976  dom2lem  7064  xpcomco  7130  pw2f1odclem  7140  php5fin  7192  elfi2  7311  supisolem  7354  inflbti  7370  inl11  7411  ismkvnex  7501  mkvprop  7504  nninfwlporlemd  7518  exmidfodomrlemreseldju  7558  ltapig  7711  ltmpig  7712  nlt1pig  7714  mulcmpblnq  7741  ltsonq  7771  lt2addnq  7777  lt2mulnq  7778  archnqq  7790  prarloclemarch  7791  ltrnqg  7793  mulcmpblnq0  7817  preqlu  7845  genpdflem  7880  addnqprllem  7900  addnqprulem  7901  addlocprlemgt  7907  appdivnq  7936  mulnqprl  7941  mulnqpru  7942  mullocprlem  7943  distrlem4prl  7957  distrlem4pru  7958  1idprl  7963  1idpru  7964  ltexprlemloc  7980  cauappcvgprlemladdrl  8030  cauappcvgprlemladd  8031  cauappcvgprlem1  8032  archrecnq  8036  caucvgprlemnkj  8039  caucvgprprlemexb  8080  addcmpblnr  8112  lttrsr  8135  ltsosr  8137  ltasrg  8143  mulextsr1  8154  srpospr  8156  caucvgsrlemcau  8166  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  map2psrprg  8178  ltresr  8212  axcaucvglemres  8272  eqlelt  8418  cnegexlem1  8508  negeu  8524  subadd2  8537  subcan2  8558  addrsub  8704  ltaddneg  8759  ltaddnegr  8760  ltadd1  8764  leadd2  8766  ltsubadd  8767  lesubadd  8769  ltaddsub2  8772  leaddsub2  8774  ltaddpos  8787  lesub2  8792  ltsub2  8794  ltnegcon1  8798  ltnegcon2  8799  lenegcon1  8801  lenegcon2  8802  addge01  8807  addge02  8808  suble0  8811  leaddle0  8812  lesub0  8814  eqord2  8819  sublt0d  8906  recexre  8914  reaplt  8924  reapltxor  8925  reapneg  8933  remulext1  8935  apreim  8939  apcotr  8943  apadd2  8945  addext  8946  apsub1  8978  mulcanap2d  8998  diveqap0  9020  diveqap1  9043  apmul2  9127  ltmul2  9194  lemul2  9195  ltmulgt11  9202  ltmulgt12  9203  gt0div  9208  ge0div  9209  ltmuldiv  9212  ltrec1  9226  lerec2  9227  ledivdiv  9228  ltdiv23  9230  lediv23  9231  suprleubex  9292  creur  9297  creui  9298  ofsubeq0  9300  nn1suc  9332  nnrecl  9572  znnsub  9705  zgt0ge1  9712  zltlen  9733  nn0n0n1ge2b  9734  nn0le2is012  9737  fcdmnn0fsuppfi  9743  btwnnz  9750  gtndiv  9751  prime  9755  eluz2  9942  indstr2  10024  negm  10030  nn01to3  10032  qapne  10054  qltlen  10055  qreccl  10057  irrmulap  10064  divlt1lt  10141  divle1le  10142  nnledivrp  10183  xnn0xadd0  10285  xltadd2  10295  xsubge0  10299  xlesubadd  10301  iccid  10343  elioc2  10354  elico2  10355  elicc2  10356  elfz2  10434  fzen  10463  fzsubel  10482  elfzp1  10495  fzpr  10500  fzrevral2  10529  fzrevral3  10530  nn0disj  10561  2ffzeq  10564  fzosplitsni  10670  fvinim0ffz  10676  ioo0  10710  ico0  10712  ioc0  10713  modq0  10786  negqmod0  10788  zmodidfzo  10810  frecuzrdgtcl  10869  nn0ennn  10890  nninfinf  10900  sq11  11069  nn0le2msqd  11178  nn0opth2d  11182  hashen  11244  zfz1isolem1  11313  zfz1iso  11314  csbwrdg  11355  wrdnval  11356  eqwrd  11366  ccat0  11385  ccatws1lenp1bg  11424  swrd0g  11453  swrdspsleq  11460  pfxeq  11489  pfxsuffeqwrdeq  11491  pfxsuff1eqwrdeq  11492  ccatopth2  11510  wrd2ind  11516  2shfti  11617  cjap  11693  cnreim  11765  rexfiuz  11776  rexanuz2  11778  abs00ap  11849  absext  11850  sqabs  11870  abslt  11876  absle  11877  absdiflt  11880  absdifle  11881  lenegsq  11883  minmax  12019  ltmininf  12024  mingeb  12032  xrminmax  12055  xrmin1inf  12057  xrmin2inf  12058  xrltmininf  12060  xrlemininf  12061  clim  12071  clim0c  12076  climrecvg1n  12138  zsumdc  12175  fsum2dlemstep  12225  binomlem  12274  pwm1geoserap1  12299  zproddc  12370  efieq  12526  sin01bnd  12548  cos01bnd  12549  dvdsval2  12581  modm1div  12591  zdvdsdc  12603  modmulconst  12614  dvdsaddr  12628  dvdsabseq  12638  fzocongeq  12649  zeo3  12659  odd2np1  12664  oddp1d2  12681  zob  12682  oddm1d2  12683  nnoddm1d2  12701  divalgb  12716  divalgmod  12718  modremain  12720  bits0  12739  bitsp1e  12743  bitsp1o  12744  bitscmp  12749  bitsinv1lem  12752  gcdn0gt0  12779  bezoutlemstep  12798  dvdssq  12832  nn0seqcvgd  12843  algcvgblem  12851  lcmdvds  12881  lcmgcdeq  12885  coprmdvds  12894  qredeq  12898  congr  12902  isprm2  12919  isprm3  12920  prmdvdsexp  12951  prmdvdsexpb  12952  prmexpb  12954  prmfac1  12955  cncongrprm  12960  nnmaxpwlemxy  12972  nnmaxpwlemnfac  12975  qnumdenbi  12996  qnumgt0  13002  hashdvds  13027  crth  13030  fermltl  13040  modprminveq  13057  pcpremul  13100  pc2dvds  13137  pcz  13139  prmpwdvds  13162  4sqlem16  13213  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemodife  13297  ballotfilemrv1  13321  ballotfilemrv2  13322  ballotfilem1ri  13335  oddennn  13340  ctinfomlemom  13375  mgm1  13748  ismhm  13826  mhmpropd  13831  issubm  13837  issubm2  13838  grpsubrcan  13944  grplactcnv  13965  grp1  13969  eqgval  14084  eqgid  14087  quselbasg  14091  isghm  14104  conjnmzb  14141  iscmn  14185  eqgabl  14223  prdsbasmpt  14286  prdsbasmpt2  14294  rngmneg1  14352  rngmneg2  14353  rngpropd  14360  rngen1zr  14366  srgen1zr0  14398  ringideu  14427  ringpropd  14449  crngpropd  14450  dvdsrd  14509  dvdsr02  14520  opprunitd  14525  crngunit  14526  unitpropdg  14563  rhmunitinv  14593  isnzr2  14599  issubrng  14615  resrhm2b  14665  aprval  14699  aprunit  14700  isdrngtap  14714  opprdrng  14728  islmod  14735  islssm  14802  islssmg  14803  ellspsn  14862  isridl  14949  zrhrhmb  15065  zndvds  15092  znleval  15096  isassa  15110  istopg  15242  eltg  15295  eltg2  15296  tgss2  15322  bastop1  15326  bastop2  15327  iscld  15346  isnei  15387  neiint  15388  iscn  15440  iscnp  15442  iscnp3  15446  tgcn  15451  ssidcn  15453  lmbr2  15457  lmbrf  15458  cnnei  15475  cnrest2  15479  eltx  15502  imasnopn  15542  ispsmet  15566  ismet  15587  isxmet  15588  metn0  15621  xmetres2  15622  elbl3ps  15637  elbl3  15638  xblpnfps  15641  xblpnf  15642  elmopn2  15692  metss  15737  bdxmet  15744  metrest  15749  xmetxp  15750  xmetxpbl  15751  metcnp3  15754  metcnp  15755  metcnp2  15756  metcn  15757  txmetcnp  15761  txmetcn  15762  metcnpd  15763  bl2ioo  15793  addcncntoplem  15804  elcncf  15816  elcncf2  15817  ivthdec  15887  ellimc3apf  15903  cnlimcim  15914  dveflem  15969  ply1termlem  15985  sincosq2sgn  16071  sinq12gt0  16074  logltb  16121  ltexp2  16194  birthdaylem3  16244  wilthlem1  16249  ppiublem1  16308  prmefexple  16325  bposlem1  16328  bposlem6  16333  bposlem7  16334  lgsdilem  16368  lgsdir2lem4  16372  lgsdir2  16374  lgsne0  16379  lgsabs1  16380  gausslemma2dlem3  16404  gausslemma2dlem7  16409  lgseisenlem3  16413  lgsquad3  16425  2lgslem1a  16429  2lgslem3c  16436  2lgslem3d  16437  2lgsoddprmlem4  16453  2sqlem7  16462  2sqlem8a  16463  uhgreq12g  16539  isuhgropm  16544  uhgr0e  16545  upgrop  16567  uhgrvtxedgiedgb  16606  isuspgropen  16627  isusgropen  16628  uhgr2edg  16669  issubgr2  16721  uhgrspansubgrlem  16739  vtxd0nedgbfi  16762  1loopgrvd0fi  16769  iswlk  16786  upgriswlkdc  16823  istrl  16848  iseupth  16910  eupth2lem2dc  16922  eupth2lem3lem3fi  16933  eupth2lem3lem4fi  16936  eupth2lem3lem7fi  16937  cbvrald  17038  bj-nalset  17143  bj-sels  17162  bj-nnelirr  17201  stnot  17261  isomninnlem  17302  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326