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  6515  mpoxopovel  6516  tpostpos  6539  smoiso  6577  frecabcl  6674  frecsuclem  6681  nnaordr  6787  nnaword  6788  nnaordex  6805  ereq1  6818  brdifun  6838  erth2  6858  qliftfun  6895  brecop  6903  elmapg  6939  elpmg  6942  mapsnd  6974  dom2lem  7062  xpcomco  7128  pw2f1odclem  7138  php5fin  7190  funisfsupp  7296  ffsuppbi  7305  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  fcdmnn0fsuppg  9629  znnsub  9707  zgt0ge1  9714  zltlen  9735  nn0n0n1ge2b  9736  nn0le2is012  9739  btwnnz  9751  gtndiv  9752  prime  9756  eluz2  9943  indstr2  10025  negm  10031  nn01to3  10033  qapne  10055  qltlen  10056  qreccl  10058  irrmulap  10065  divlt1lt  10142  divle1le  10143  nnledivrp  10184  xnn0xadd0  10286  xltadd2  10296  xsubge0  10300  xlesubadd  10302  iccid  10344  elioc2  10355  elico2  10356  elicc2  10357  elfz2  10435  fzen  10464  fzsubel  10483  elfzp1  10496  fzpr  10501  fzrevral2  10530  fzrevral3  10531  nn0disj  10562  2ffzeq  10565  fzosplitsni  10671  fvinim0ffz  10677  ioo0  10711  ico0  10713  ioc0  10714  modq0  10787  negqmod0  10789  zmodidfzo  10811  frecuzrdgtcl  10870  nn0ennn  10891  nninfinf  10901  sq11  11070  nn0le2msqd  11179  nn0opth2d  11183  hashen  11245  zfz1isolem1  11314  zfz1iso  11315  csbwrdg  11356  wrdnval  11357  eqwrd  11367  ccat0  11386  ccatws1lenp1bg  11425  swrd0g  11454  swrdspsleq  11461  pfxeq  11490  pfxsuffeqwrdeq  11492  pfxsuff1eqwrdeq  11493  ccatopth2  11511  wrd2ind  11517  2shfti  11618  cjap  11694  cnreim  11766  rexfiuz  11777  rexanuz2  11779  abs00ap  11850  absext  11851  sqabs  11871  abslt  11877  absle  11878  absdiflt  11881  absdifle  11882  lenegsq  11884  minmax  12020  ltmininf  12025  mingeb  12033  xrminmax  12056  xrmin1inf  12058  xrmin2inf  12059  xrltmininf  12061  xrlemininf  12062  clim  12072  clim0c  12077  climrecvg1n  12139  zsumdc  12176  fsum2dlemstep  12226  binomlem  12275  pwm1geoserap1  12300  zproddc  12371  efieq  12527  sin01bnd  12549  cos01bnd  12550  dvdsval2  12582  modm1div  12592  zdvdsdc  12604  modmulconst  12615  dvdsaddr  12629  dvdsabseq  12639  fzocongeq  12650  zeo3  12660  odd2np1  12665  oddp1d2  12682  zob  12683  oddm1d2  12684  nnoddm1d2  12702  divalgb  12717  divalgmod  12719  modremain  12721  bits0  12740  bitsp1e  12744  bitsp1o  12745  bitscmp  12750  bitsinv1lem  12753  gcdn0gt0  12780  bezoutlemstep  12799  dvdssq  12833  nn0seqcvgd  12844  algcvgblem  12852  lcmdvds  12882  lcmgcdeq  12886  coprmdvds  12895  qredeq  12899  congr  12903  isprm2  12920  isprm3  12921  prmdvdsexp  12952  prmdvdsexpb  12953  prmexpb  12955  prmfac1  12956  cncongrprm  12961  nnmaxpwlemxy  12973  nnmaxpwlemnfac  12976  qnumdenbi  12997  qnumgt0  13003  hashdvds  13028  crth  13031  fermltl  13041  modprminveq  13058  pcpremul  13101  pc2dvds  13138  pcz  13140  prmpwdvds  13163  4sqlem16  13214  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  ballotfilemrv1  13322  ballotfilemrv2  13323  ballotfilem1ri  13336  oddennn  13341  ctinfomlemom  13376  mgm1  13749  ismhm  13827  mhmpropd  13832  issubm  13838  issubm2  13839  grpsubrcan  13945  grplactcnv  13966  grp1  13970  eqgval  14085  eqgid  14088  quselbasg  14092  isghm  14105  conjnmzb  14142  iscmn  14186  eqgabl  14224  prdsbasmpt  14287  prdsbasmpt2  14295  rngmneg1  14353  rngmneg2  14354  rngpropd  14361  rngen1zr  14367  srgen1zr0  14399  ringideu  14428  ringpropd  14450  crngpropd  14451  dvdsrd  14510  dvdsr02  14521  opprunitd  14526  crngunit  14527  unitpropdg  14564  rhmunitinv  14594  isnzr2  14600  issubrng  14616  resrhm2b  14666  aprval  14700  aprunit  14701  isdrngtap  14715  opprdrng  14729  islmod  14736  islssm  14803  islssmg  14804  ellspsn  14863  isridl  14950  zrhrhmb  15066  zndvds  15093  znleval  15097  isassa  15111  istopg  15225  eltg  15278  eltg2  15279  tgss2  15305  bastop1  15309  bastop2  15310  iscld  15329  isnei  15370  neiint  15371  iscn  15423  iscnp  15425  iscnp3  15429  tgcn  15434  ssidcn  15436  lmbr2  15440  lmbrf  15441  cnnei  15458  cnrest2  15462  eltx  15485  imasnopn  15525  ispsmet  15549  ismet  15570  isxmet  15571  metn0  15604  xmetres2  15605  elbl3ps  15620  elbl3  15621  xblpnfps  15624  xblpnf  15625  elmopn2  15675  metss  15720  bdxmet  15727  metrest  15732  xmetxp  15733  xmetxpbl  15734  metcnp3  15737  metcnp  15738  metcnp2  15739  metcn  15740  txmetcnp  15744  txmetcn  15745  metcnpd  15746  bl2ioo  15776  addcncntoplem  15787  elcncf  15799  elcncf2  15800  ivthdec  15870  ellimc3apf  15886  cnlimcim  15897  dveflem  15952  ply1termlem  15968  sincosq2sgn  16054  sinq12gt0  16057  logltb  16104  ltexp2  16177  birthdaylem3  16227  wilthlem1  16232  ppiublem1  16291  prmefexple  16308  bposlem1  16311  bposlem6  16316  bposlem7  16317  lgsdilem  16351  lgsdir2lem4  16355  lgsdir2  16357  lgsne0  16362  lgsabs1  16363  gausslemma2dlem3  16387  gausslemma2dlem7  16392  lgseisenlem3  16396  lgsquad3  16408  2lgslem1a  16412  2lgslem3c  16419  2lgslem3d  16420  2lgsoddprmlem4  16436  2sqlem7  16445  2sqlem8a  16446  uhgreq12g  16522  isuhgropm  16527  uhgr0e  16528  upgrop  16550  uhgrvtxedgiedgb  16589  isuspgropen  16610  isusgropen  16611  uhgr2edg  16652  issubgr2  16704  uhgrspansubgrlem  16722  vtxd0nedgbfi  16745  1loopgrvd0fi  16752  iswlk  16769  upgriswlkdc  16806  istrl  16831  iseupth  16893  eupth2lem2dc  16905  eupth2lem3lem3fi  16916  eupth2lem3lem4fi  16919  eupth2lem3lem7fi  16920  cbvrald  17021  bj-nalset  17126  bj-sels  17145  bj-nnelirr  17184  stnot  17244  isomninnlem  17285  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309