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  801  con1biidc  885  pm4.54dc  910  dn1dc  969  dedlem0a  977  dfifp3dc  991  dfifp4dc  992  dfifp5dc  993  3bior2fd  1391  xorbi12d  1427  nbbndc  1439  eleq12d  2303  neeq12d  2432  neleq12d  2513  raleqbi1dv  2753  rexeqbi1dv  2754  reueqd  2755  rmoeqd  2756  raleqbidv  2757  rexeqbidv  2758  raleqbidva  2759  rexeqbidva  2760  eueq3dc  2991  sbc19.21g  3111  sbcabel  3125  sbcel1g  3157  sbceq1g  3158  sbcel2g  3159  sbceq2g  3160  sbccsb2g  3168  sbcco3g  3196  sseq12d  3269  raaanlem  3614  sbcssg  3618  ralsng  3729  2ralunsn  3903  csbunig  3922  disjeq12d  4094  breq123d  4123  sbcbr12g  4165  sbcbr1g  4166  sbcbr2g  4167  treq  4214  nalset  4240  exmidsssn  4315  copsex4g  4363  onsucb  4625  posng  4822  csbxpg  4831  sbcrel  4836  csbcnvg  4939  eliniseg  5132  brcodir  5150  csbrng  5224  sbcfung  5376  fneq12d  5448  feq12d  5498  feq123d  5499  sbcfng  5506  sbcfg  5507  f1osng  5657  csbfv12g  5710  funimass4  5727  dmfco  5745  eqfnfv  5775  eqfnfv2  5776  fneqeql2  5787  fvimacnvi  5792  funimass3  5794  fniniseg  5798  unpreima  5802  ralrnmpt  5819  rexrnmpt  5820  dffo3  5824  fmptco  5843  fressnfv  5871  eufnfv  5917  foima2  5924  fnunirn  5940  dff13  5941  f1elima  5946  cocan1  5960  cocan2  5961  fliftel  5966  fliftf  5972  isoresbr  5982  isoini  5991  f1oiso  5999  f1ofveu  6038  mpoeq123dva  6114  ovid  6170  ov  6173  ovg  6193  ovelrn  6203  caovord2d  6224  ofrfval2  6283  offveqb  6286  eqop  6371  reldm  6380  f1od2  6431  suppval1  6439  suppssrst  6461  suppssrgst  6462  mpoxopoveq  6471  mpoxopovel  6472  tpostpos  6495  smoiso  6533  frecabcl  6630  frecsuclem  6637  nnaordr  6743  nnaword  6744  nnaordex  6761  ereq1  6774  brdifun  6794  erth2  6814  qliftfun  6851  brecop  6859  elmapg  6895  elpmg  6898  mapsnd  6923  dom2lem  7011  xpcomco  7077  pw2f1odclem  7087  php5fin  7139  funisfsupp  7244  ffsuppbi  7253  elfi2  7259  supisolem  7299  inflbti  7315  inl11  7356  ismkvnex  7446  mkvprop  7449  nninfwlporlemd  7463  exmidfodomrlemreseldju  7503  ltapig  7653  ltmpig  7654  nlt1pig  7656  mulcmpblnq  7683  ltsonq  7713  lt2addnq  7719  lt2mulnq  7720  archnqq  7732  prarloclemarch  7733  ltrnqg  7735  mulcmpblnq0  7759  preqlu  7787  genpdflem  7822  addnqprllem  7842  addnqprulem  7843  addlocprlemgt  7849  appdivnq  7878  mulnqprl  7883  mulnqpru  7884  mullocprlem  7885  distrlem4prl  7899  distrlem4pru  7900  1idprl  7905  1idpru  7906  ltexprlemloc  7922  cauappcvgprlemladdrl  7972  cauappcvgprlemladd  7973  cauappcvgprlem1  7974  archrecnq  7978  caucvgprlemnkj  7981  caucvgprprlemexb  8022  addcmpblnr  8054  lttrsr  8077  ltsosr  8079  ltasrg  8085  mulextsr1  8096  srpospr  8098  caucvgsrlemcau  8108  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  map2psrprg  8120  ltresr  8154  axcaucvglemres  8214  eqlelt  8360  cnegexlem1  8448  negeu  8464  subadd2  8477  subcan2  8498  addrsub  8644  ltaddneg  8698  ltaddnegr  8699  ltadd1  8703  leadd2  8705  ltsubadd  8706  lesubadd  8708  ltaddsub2  8711  leaddsub2  8713  ltaddpos  8726  lesub2  8731  ltsub2  8733  ltnegcon1  8737  ltnegcon2  8738  lenegcon1  8740  lenegcon2  8741  addge01  8746  addge02  8747  suble0  8750  leaddle0  8751  lesub0  8753  eqord2  8758  sublt0d  8844  recexre  8852  reaplt  8862  reapltxor  8863  reapneg  8871  remulext1  8873  apreim  8877  apcotr  8881  apadd2  8883  addext  8884  apsub1  8916  mulcanap2d  8936  diveqap0  8956  diveqap1  8979  apmul2  9063  ltmul2  9130  lemul2  9131  ltmulgt11  9138  ltmulgt12  9139  gt0div  9144  ge0div  9145  ltmuldiv  9148  ltrec1  9162  lerec2  9163  ledivdiv  9164  ltdiv23  9166  lediv23  9167  suprleubex  9228  creur  9233  creui  9234  nn1suc  9256  nnrecl  9494  fcdmnn0fsuppg  9551  znnsub  9629  zgt0ge1  9636  zltlen  9656  nn0n0n1ge2b  9657  nn0le2is012  9660  btwnnz  9672  gtndiv  9673  prime  9677  eluz2  9859  indstr2  9941  negm  9947  nn01to3  9949  qapne  9971  qltlen  9972  qreccl  9974  irrmulap  9980  divlt1lt  10057  divle1le  10058  nnledivrp  10099  xnn0xadd0  10200  xltadd2  10210  xsubge0  10214  xlesubadd  10216  iccid  10258  elioc2  10269  elico2  10270  elicc2  10271  elfz2  10349  fzen  10377  fzsubel  10394  elfzp1  10406  fzpr  10411  fzrevral2  10440  fzrevral3  10441  nn0disj  10472  2ffzeq  10475  fzosplitsni  10581  fvinim0ffz  10587  ioo0  10619  ico0  10621  ioc0  10622  modq0  10691  negqmod0  10693  zmodidfzo  10715  frecuzrdgtcl  10774  nn0ennn  10795  nninfinf  10805  sq11  10974  nn0le2msqd  11081  nn0opth2d  11085  hashen  11147  zfz1isolem1  11212  zfz1iso  11213  csbwrdg  11254  wrdnval  11255  eqwrd  11265  ccat0  11284  ccatws1lenp1bg  11323  swrd0g  11352  swrdspsleq  11359  pfxeq  11388  pfxsuffeqwrdeq  11390  pfxsuff1eqwrdeq  11391  ccatopth2  11409  wrd2ind  11415  2shfti  11516  cjap  11591  cnreim  11663  rexfiuz  11674  rexanuz2  11676  abs00ap  11747  absext  11748  sqabs  11767  abslt  11773  absle  11774  absdiflt  11777  absdifle  11778  lenegsq  11780  minmax  11915  ltmininf  11920  mingeb  11927  xrminmax  11950  xrmin1inf  11952  xrmin2inf  11953  xrltmininf  11955  xrlemininf  11956  clim  11966  clim0c  11971  climrecvg1n  12033  zsumdc  12070  fsum2dlemstep  12120  binomlem  12169  pwm1geoserap1  12194  zproddc  12265  efieq  12421  sin01bnd  12443  cos01bnd  12444  dvdsval2  12476  modm1div  12486  zdvdsdc  12498  modmulconst  12509  dvdsaddr  12523  dvdsabseq  12533  fzocongeq  12544  zeo3  12554  odd2np1  12559  oddp1d2  12576  zob  12577  oddm1d2  12578  nnoddm1d2  12596  divalgb  12611  divalgmod  12613  modremain  12615  bits0  12634  bitsp1e  12638  bitsp1o  12639  bitscmp  12644  bitsinv1lem  12647  gcdn0gt0  12674  bezoutlemstep  12693  dvdssq  12727  nn0seqcvgd  12738  algcvgblem  12746  lcmdvds  12776  lcmgcdeq  12780  coprmdvds  12789  qredeq  12793  congr  12797  isprm2  12814  isprm3  12815  prmdvdsexp  12845  prmdvdsexpb  12846  prmexpb  12848  prmfac1  12849  cncongrprm  12854  oddpwdclemxy  12866  oddpwdclemodd  12869  qnumdenbi  12889  qnumgt0  12895  hashdvds  12918  crth  12921  fermltl  12931  modprminveq  12948  pcpremul  12991  pc2dvds  13028  pcz  13030  prmpwdvds  13053  4sqlem16  13104  oddennn  13143  ctinfomlemom  13178  prdsbasmpt  13493  prdsbasmpt2  13501  mgm1  13583  ismhm  13674  mhmpropd  13679  issubm  13685  issubm2  13686  grpsubrcan  13794  grplactcnv  13815  grp1  13819  eqgval  13940  eqgid  13943  quselbasg  13947  isghm  13960  conjnmzb  13997  iscmn  14010  eqgabl  14047  rngmneg1  14091  rngmneg2  14092  rngpropd  14099  srgen1zr  14132  ringideu  14161  ringpropd  14182  crngpropd  14183  dvdsrd  14239  dvdsr02  14250  opprunitd  14255  crngunit  14256  unitpropdg  14293  rhmunitinv  14323  isnzr2  14329  issubrng  14344  resrhm2b  14394  aprval  14428  islmod  14439  islssm  14505  islssmg  14506  ellspsn  14565  isridl  14652  zrhrhmb  14770  zndvds  14797  znleval  14801  istopg  14864  eltg  14917  eltg2  14918  tgss2  14944  bastop1  14948  bastop2  14949  iscld  14968  isnei  15009  neiint  15010  iscn  15062  iscnp  15064  iscnp3  15068  tgcn  15073  ssidcn  15075  lmbr2  15079  lmbrf  15080  cnnei  15097  cnrest2  15101  eltx  15124  imasnopn  15164  ispsmet  15188  ismet  15209  isxmet  15210  metn0  15243  xmetres2  15244  elbl3ps  15259  elbl3  15260  xblpnfps  15263  xblpnf  15264  elmopn2  15314  metss  15359  bdxmet  15366  metrest  15371  xmetxp  15372  xmetxpbl  15373  metcnp3  15376  metcnp  15377  metcnp2  15378  metcn  15379  txmetcnp  15383  txmetcn  15384  metcnpd  15385  bl2ioo  15415  addcncntoplem  15426  elcncf  15438  elcncf2  15439  ivthdec  15509  ellimc3apf  15525  cnlimcim  15536  dveflem  15591  ply1termlem  15607  sincosq2sgn  15692  sinq12gt0  15695  logltb  15739  ltexp2  15806  wilthlem1  15848  lgsdilem  15900  lgsdir2lem4  15904  lgsdir2  15906  lgsne0  15911  lgsabs1  15912  gausslemma2dlem3  15936  gausslemma2dlem7  15941  lgseisenlem3  15945  lgsquad3  15957  2lgslem1a  15961  2lgslem3c  15968  2lgslem3d  15969  2lgsoddprmlem4  15985  2sqlem7  15994  2sqlem8a  15995  uhgreq12g  16071  isuhgropm  16076  uhgr0e  16077  upgrop  16099  uhgrvtxedgiedgb  16138  isuspgropen  16159  isusgropen  16160  uhgr2edg  16201  issubgr2  16253  uhgrspansubgrlem  16271  vtxd0nedgbfi  16294  1loopgrvd0fi  16301  iswlk  16318  upgriswlkdc  16355  istrl  16380  iseupth  16442  eupth2lem2dc  16454  eupth2lem3lem3fi  16465  eupth2lem3lem4fi  16468  eupth2lem3lem7fi  16469  cbvrald  16560  bj-nalset  16665  bj-sels  16684  bj-nnelirr  16723  isomninnlem  16814  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837