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  794  con1biidc  878  pm4.54dc  903  dn1dc  962  dedlem0a  970  xorbi12d  1393  nbbndc  1405  eleq12d  2267  neeq12d  2387  neleq12d  2468  raleqbi1dv  2705  rexeqbi1dv  2706  reueqd  2707  rmoeqd  2708  raleqbidv  2709  rexeqbidv  2710  raleqbidva  2711  rexeqbidva  2712  eueq3dc  2938  sbc19.21g  3058  sbcabel  3071  sbcel1g  3103  sbceq1g  3104  sbcel2g  3105  sbceq2g  3106  sbccsb2g  3114  sbcco3g  3142  sseq12d  3214  raaanlem  3555  sbcssg  3559  ralsng  3662  2ralunsn  3828  csbunig  3847  disjeq12d  4019  breq123d  4047  sbcbr12g  4088  sbcbr1g  4089  sbcbr2g  4090  treq  4137  nalset  4163  exmidsssn  4235  copsex4g  4280  onsucb  4539  posng  4735  csbxpg  4744  sbcrel  4749  csbcnvg  4850  eliniseg  5039  brcodir  5057  csbrng  5131  sbcfung  5282  fneq12d  5350  feq12d  5397  feq123d  5398  sbcfng  5405  sbcfg  5406  f1osng  5545  csbfv12g  5596  funimass4  5611  dmfco  5629  eqfnfv  5659  eqfnfv2  5660  fneqeql2  5671  fvimacnvi  5676  funimass3  5678  fniniseg  5682  rexsupp  5686  unpreima  5687  ralrnmpt  5704  rexrnmpt  5705  dffo3  5709  fmptco  5728  fressnfv  5749  eufnfv  5793  foima2  5798  fnunirn  5814  dff13  5815  f1elima  5820  cocan1  5834  cocan2  5835  fliftel  5840  fliftf  5846  isoresbr  5856  isoini  5865  f1oiso  5873  f1ofveu  5910  mpoeq123dva  5983  ovid  6039  ov  6042  ovg  6062  ovelrn  6072  caovord2d  6093  ofrfval2  6152  offveqb  6155  eqop  6235  reldm  6244  f1od2  6293  mpoxopoveq  6298  mpoxopovel  6299  tpostpos  6322  smoiso  6360  frecabcl  6457  frecsuclem  6464  nnaordr  6568  nnaword  6569  nnaordex  6586  ereq1  6599  brdifun  6619  erth2  6639  qliftfun  6676  brecop  6684  elmapg  6720  elpmg  6723  dom2lem  6831  xpcomco  6885  pw2f1odclem  6895  php5fin  6943  elfi2  7038  supisolem  7074  inflbti  7090  inl11  7131  ismkvnex  7221  mkvprop  7224  nninfwlporlemd  7238  exmidfodomrlemreseldju  7267  ltapig  7405  ltmpig  7406  nlt1pig  7408  mulcmpblnq  7435  ltsonq  7465  lt2addnq  7471  lt2mulnq  7472  archnqq  7484  prarloclemarch  7485  ltrnqg  7487  mulcmpblnq0  7511  preqlu  7539  genpdflem  7574  addnqprllem  7594  addnqprulem  7595  addlocprlemgt  7601  appdivnq  7630  mulnqprl  7635  mulnqpru  7636  mullocprlem  7637  distrlem4prl  7651  distrlem4pru  7652  1idprl  7657  1idpru  7658  ltexprlemloc  7674  cauappcvgprlemladdrl  7724  cauappcvgprlemladd  7725  cauappcvgprlem1  7726  archrecnq  7730  caucvgprlemnkj  7733  caucvgprprlemexb  7774  addcmpblnr  7806  lttrsr  7829  ltsosr  7831  ltasrg  7837  mulextsr1  7848  srpospr  7850  caucvgsrlemcau  7860  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  map2psrprg  7872  ltresr  7906  axcaucvglemres  7966  eqlelt  8113  cnegexlem1  8201  negeu  8217  subadd2  8230  subcan2  8251  addrsub  8397  ltaddneg  8451  ltaddnegr  8452  ltadd1  8456  leadd2  8458  ltsubadd  8459  lesubadd  8461  ltaddsub2  8464  leaddsub2  8466  ltaddpos  8479  lesub2  8484  ltsub2  8486  ltnegcon1  8490  ltnegcon2  8491  lenegcon1  8493  lenegcon2  8494  addge01  8499  addge02  8500  suble0  8503  leaddle0  8504  lesub0  8506  eqord2  8511  sublt0d  8597  recexre  8605  reaplt  8615  reapltxor  8616  reapneg  8624  remulext1  8626  apreim  8630  apcotr  8634  apadd2  8636  addext  8637  apsub1  8669  mulcanap2d  8689  diveqap0  8709  diveqap1  8732  apmul2  8816  ltmul2  8883  lemul2  8884  ltmulgt11  8891  ltmulgt12  8892  gt0div  8897  ge0div  8898  ltmuldiv  8901  ltrec1  8915  lerec2  8916  ledivdiv  8917  ltdiv23  8919  lediv23  8920  suprleubex  8981  creur  8986  creui  8987  nn1suc  9009  nnrecl  9247  znnsub  9377  zgt0ge1  9384  zltlen  9404  nn0n0n1ge2b  9405  nn0le2is012  9408  btwnnz  9420  gtndiv  9421  prime  9425  eluz2  9607  indstr2  9683  negm  9689  nn01to3  9691  qapne  9713  qltlen  9714  qreccl  9716  irrmulap  9722  divlt1lt  9799  divle1le  9800  nnledivrp  9841  xnn0xadd0  9942  xltadd2  9952  xsubge0  9956  xlesubadd  9958  iccid  10000  elioc2  10011  elico2  10012  elicc2  10013  elfz2  10090  fzen  10118  fzsubel  10135  elfzp1  10147  fzpr  10152  fzrevral2  10181  fzrevral3  10182  nn0disj  10213  2ffzeq  10216  fzosplitsni  10311  fvinim0ffz  10317  ioo0  10349  ico0  10351  ioc0  10352  modq0  10421  negqmod0  10423  zmodidfzo  10445  frecuzrdgtcl  10504  nn0ennn  10525  nninfinf  10535  sq11  10704  nn0le2msqd  10811  nn0opth2d  10815  hashen  10876  zfz1isolem1  10932  zfz1iso  10933  csbwrdg  10964  wrdnval  10965  eqwrd  10975  2shfti  10996  cjap  11071  cnreim  11143  rexfiuz  11154  rexanuz2  11156  abs00ap  11227  absext  11228  sqabs  11247  abslt  11253  absle  11254  absdiflt  11257  absdifle  11258  lenegsq  11260  minmax  11395  ltmininf  11400  mingeb  11407  xrminmax  11430  xrmin1inf  11432  xrmin2inf  11433  xrltmininf  11435  xrlemininf  11436  clim  11446  clim0c  11451  climrecvg1n  11513  zsumdc  11549  fsum2dlemstep  11599  binomlem  11648  pwm1geoserap1  11673  zproddc  11744  efieq  11900  sin01bnd  11922  cos01bnd  11923  dvdsval2  11955  modm1div  11965  zdvdsdc  11977  modmulconst  11988  dvdsaddr  12002  dvdsabseq  12012  fzocongeq  12023  zeo3  12033  odd2np1  12038  oddp1d2  12055  zob  12056  oddm1d2  12057  nnoddm1d2  12075  divalgb  12090  divalgmod  12092  modremain  12094  bits0  12112  bitsp1e  12116  bitsp1o  12117  gcdn0gt0  12145  bezoutlemstep  12164  dvdssq  12198  nn0seqcvgd  12209  algcvgblem  12217  lcmdvds  12247  lcmgcdeq  12251  coprmdvds  12260  qredeq  12264  congr  12268  isprm2  12285  isprm3  12286  prmdvdsexp  12316  prmdvdsexpb  12317  prmexpb  12319  prmfac1  12320  cncongrprm  12325  oddpwdclemxy  12337  oddpwdclemodd  12340  qnumdenbi  12360  qnumgt0  12366  hashdvds  12389  crth  12392  fermltl  12402  modprminveq  12419  pcpremul  12462  pc2dvds  12499  pcz  12501  prmpwdvds  12524  4sqlem16  12575  oddennn  12609  ctinfomlemom  12644  mgm1  13013  ismhm  13093  mhmpropd  13098  issubm  13104  issubm2  13105  grpsubrcan  13213  grplactcnv  13234  grp1  13238  eqgval  13353  eqgid  13356  quselbasg  13360  isghm  13373  conjnmzb  13410  iscmn  13423  eqgabl  13460  rngmneg1  13503  rngmneg2  13504  rngpropd  13511  srgen1zr  13544  ringideu  13573  ringpropd  13594  crngpropd  13595  dvdsrd  13650  dvdsr02  13661  opprunitd  13666  crngunit  13667  unitpropdg  13704  rhmunitinv  13734  isnzr2  13740  issubrng  13755  resrhm2b  13805  aprval  13838  islmod  13847  islssm  13913  islssmg  13914  ellspsn  13973  isridl  14060  zrhrhmb  14178  zndvds  14205  znleval  14209  istopg  14235  eltg  14288  eltg2  14289  tgss2  14315  bastop1  14319  bastop2  14320  iscld  14339  isnei  14380  neiint  14381  iscn  14433  iscnp  14435  iscnp3  14439  tgcn  14444  ssidcn  14446  lmbr2  14450  lmbrf  14451  cnnei  14468  cnrest2  14472  eltx  14495  imasnopn  14535  ispsmet  14559  ismet  14580  isxmet  14581  metn0  14614  xmetres2  14615  elbl3ps  14630  elbl3  14631  xblpnfps  14634  xblpnf  14635  elmopn2  14685  metss  14730  bdxmet  14737  metrest  14742  xmetxp  14743  xmetxpbl  14744  metcnp3  14747  metcnp  14748  metcnp2  14749  metcn  14750  txmetcnp  14754  txmetcn  14755  metcnpd  14756  bl2ioo  14786  addcncntoplem  14797  elcncf  14809  elcncf2  14810  ivthdec  14880  ellimc3apf  14896  cnlimcim  14907  dveflem  14962  ply1termlem  14978  sincosq2sgn  15063  sinq12gt0  15066  logltb  15110  ltexp2  15177  wilthlem1  15216  lgsdilem  15268  lgsdir2lem4  15272  lgsdir2  15274  lgsne0  15279  lgsabs1  15280  gausslemma2dlem3  15304  gausslemma2dlem7  15309  lgseisenlem3  15313  lgsquad3  15325  2lgslem1a  15329  2lgslem3c  15336  2lgslem3d  15337  2lgsoddprmlem4  15353  2sqlem7  15362  2sqlem8a  15363  cbvrald  15434  bj-nalset  15541  bj-sels  15560  bj-nnelirr  15599  isomninnlem  15674  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696