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  793  con1biidc  877  pm4.54dc  902  dn1dc  960  dedlem0a  968  xorbi12d  1382  nbbndc  1394  eleq12d  2248  neeq12d  2367  neleq12d  2448  raleqbi1dv  2681  rexeqbi1dv  2682  reueqd  2683  rmoeqd  2684  raleqbidv  2685  rexeqbidv  2686  raleqbidva  2687  rexeqbidva  2688  eueq3dc  2912  sbc19.21g  3032  sbcabel  3045  sbcel1g  3077  sbceq1g  3078  sbcel2g  3079  sbceq2g  3080  sbccsb2g  3088  sbcco3g  3115  sseq12d  3187  raaanlem  3529  sbcssg  3533  ralsng  3633  2ralunsn  3799  csbunig  3818  disjeq12d  3990  breq123d  4018  sbcbr12g  4059  sbcbr1g  4060  sbcbr2g  4061  treq  4108  nalset  4134  exmidsssn  4203  copsex4g  4248  onsucb  4503  posng  4699  csbxpg  4708  sbcrel  4713  csbcnvg  4812  eliniseg  4999  brcodir  5017  csbrng  5091  sbcfung  5241  fneq12d  5309  feq12d  5356  feq123d  5357  sbcfng  5364  sbcfg  5365  f1osng  5503  csbfv12g  5552  funimass4  5567  dmfco  5585  eqfnfv  5614  eqfnfv2  5615  fneqeql2  5626  fvimacnvi  5631  funimass3  5633  fniniseg  5637  rexsupp  5641  unpreima  5642  ralrnmpt  5659  rexrnmpt  5660  dffo3  5664  fmptco  5683  fressnfv  5704  eufnfv  5748  foima2  5753  fnunirn  5768  dff13  5769  f1elima  5774  cocan1  5788  cocan2  5789  fliftel  5794  fliftf  5800  isoresbr  5810  isoini  5819  f1oiso  5827  f1ofveu  5863  mpoeq123dva  5936  ovid  5991  ov  5994  ovg  6013  ovelrn  6023  caovord2d  6044  ofrfval2  6099  offveqb  6102  eqop  6178  reldm  6187  f1od2  6236  mpoxopoveq  6241  mpoxopovel  6242  tpostpos  6265  smoiso  6303  frecabcl  6400  frecsuclem  6407  nnaordr  6511  nnaword  6512  nnaordex  6529  ereq1  6542  brdifun  6562  erth2  6580  qliftfun  6617  brecop  6625  elmapg  6661  elpmg  6664  dom2lem  6772  xpcomco  6826  php5fin  6882  elfi2  6971  supisolem  7007  inflbti  7023  inl11  7064  ismkvnex  7153  mkvprop  7156  nninfwlporlemd  7170  exmidfodomrlemreseldju  7199  ltapig  7337  ltmpig  7338  nlt1pig  7340  mulcmpblnq  7367  ltsonq  7397  lt2addnq  7403  lt2mulnq  7404  archnqq  7416  prarloclemarch  7417  ltrnqg  7419  mulcmpblnq0  7443  preqlu  7471  genpdflem  7506  addnqprllem  7526  addnqprulem  7527  addlocprlemgt  7533  appdivnq  7562  mulnqprl  7567  mulnqpru  7568  mullocprlem  7569  distrlem4prl  7583  distrlem4pru  7584  1idprl  7589  1idpru  7590  ltexprlemloc  7606  cauappcvgprlemladdrl  7656  cauappcvgprlemladd  7657  cauappcvgprlem1  7658  archrecnq  7662  caucvgprlemnkj  7665  caucvgprprlemexb  7706  addcmpblnr  7738  lttrsr  7761  ltsosr  7763  ltasrg  7769  mulextsr1  7780  srpospr  7782  caucvgsrlemcau  7792  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  map2psrprg  7804  ltresr  7838  axcaucvglemres  7898  eqlelt  8044  cnegexlem1  8132  negeu  8148  subadd2  8161  subcan2  8182  addrsub  8328  ltaddneg  8381  ltaddnegr  8382  ltadd1  8386  leadd2  8388  ltsubadd  8389  lesubadd  8391  ltaddsub2  8394  leaddsub2  8396  ltaddpos  8409  lesub2  8414  ltsub2  8416  ltnegcon1  8420  ltnegcon2  8421  lenegcon1  8423  lenegcon2  8424  addge01  8429  addge02  8430  suble0  8433  leaddle0  8434  lesub0  8436  eqord2  8441  sublt0d  8527  recexre  8535  reaplt  8545  reapltxor  8546  reapneg  8554  remulext1  8556  apreim  8560  apcotr  8564  apadd2  8566  addext  8567  apsub1  8599  mulcanap2d  8619  diveqap0  8639  diveqap1  8662  apmul2  8746  ltmul2  8813  lemul2  8814  ltmulgt11  8821  ltmulgt12  8822  gt0div  8827  ge0div  8828  ltmuldiv  8831  ltrec1  8845  lerec2  8846  ledivdiv  8847  ltdiv23  8849  lediv23  8850  suprleubex  8911  creur  8916  creui  8917  nn1suc  8938  nnrecl  9174  znnsub  9304  zgt0ge1  9311  zltlen  9331  nn0n0n1ge2b  9332  nn0le2is012  9335  btwnnz  9347  gtndiv  9348  prime  9352  eluz2  9534  indstr2  9609  negm  9615  nn01to3  9617  qapne  9639  qltlen  9640  qreccl  9642  divlt1lt  9724  divle1le  9725  nnledivrp  9766  xnn0xadd0  9867  xltadd2  9877  xsubge0  9881  xlesubadd  9883  iccid  9925  elioc2  9936  elico2  9937  elicc2  9938  elfz2  10015  fzen  10043  fzsubel  10060  elfzp1  10072  fzpr  10077  fzrevral2  10106  fzrevral3  10107  nn0disj  10138  2ffzeq  10141  fzosplitsni  10235  fvinim0ffz  10241  ioo0  10260  ico0  10262  ioc0  10263  modq0  10329  negqmod0  10331  zmodidfzo  10353  frecuzrdgtcl  10412  nn0ennn  10433  sq11  10593  nn0le2msqd  10699  nn0opth2d  10703  hashen  10764  zfz1isolem1  10820  zfz1iso  10821  2shfti  10840  cjap  10915  cnreim  10987  rexfiuz  10998  rexanuz2  11000  abs00ap  11071  absext  11072  sqabs  11091  abslt  11097  absle  11098  absdiflt  11101  absdifle  11102  lenegsq  11104  minmax  11238  ltmininf  11243  mingeb  11250  xrminmax  11273  xrmin1inf  11275  xrmin2inf  11276  xrltmininf  11278  xrlemininf  11279  clim  11289  clim0c  11294  climrecvg1n  11356  zsumdc  11392  fsum2dlemstep  11442  binomlem  11491  pwm1geoserap1  11516  zproddc  11587  efieq  11743  sin01bnd  11765  cos01bnd  11766  dvdsval2  11797  modm1div  11807  zdvdsdc  11819  modmulconst  11830  dvdsaddr  11844  dvdsabseq  11853  fzocongeq  11864  zeo3  11873  odd2np1  11878  oddp1d2  11895  zob  11896  oddm1d2  11897  nnoddm1d2  11915  divalgb  11930  divalgmod  11932  modremain  11934  gcdn0gt0  11979  bezoutlemstep  11998  dvdssq  12032  nn0seqcvgd  12041  algcvgblem  12049  lcmdvds  12079  lcmgcdeq  12083  coprmdvds  12092  qredeq  12096  congr  12100  isprm2  12117  isprm3  12118  prmdvdsexp  12148  prmdvdsexpb  12149  prmexpb  12151  prmfac1  12152  cncongrprm  12157  oddpwdclemxy  12169  oddpwdclemodd  12172  qnumdenbi  12192  qnumgt0  12198  hashdvds  12221  crth  12224  fermltl  12234  modprminveq  12250  pcpremul  12293  pc2dvds  12329  pcz  12331  prmpwdvds  12353  oddennn  12393  ctinfomlemom  12428  mgm1  12789  ismhm  12853  mhmpropd  12857  issubm  12863  issubm2  12864  grpsubrcan  12951  grplactcnv  12972  grp1  12976  eqgval  13082  eqgid  13085  iscmn  13096  srgen1zr  13171  ringideu  13200  ringpropd  13217  crngpropd  13218  dvdsrd  13263  dvdsr02  13274  opprunitd  13279  crngunit  13280  unitpropdg  13317  aprval  13372  islmod  13381  istopg  13502  eltg  13555  eltg2  13556  tgss2  13582  bastop1  13586  bastop2  13587  iscld  13606  isnei  13647  neiint  13648  iscn  13700  iscnp  13702  iscnp3  13706  tgcn  13711  ssidcn  13713  lmbr2  13717  lmbrf  13718  cnnei  13735  cnrest2  13739  eltx  13762  imasnopn  13802  ispsmet  13826  ismet  13847  isxmet  13848  metn0  13881  xmetres2  13882  elbl3ps  13897  elbl3  13898  xblpnfps  13901  xblpnf  13902  elmopn2  13952  metss  13997  bdxmet  14004  metrest  14009  xmetxp  14010  xmetxpbl  14011  metcnp3  14014  metcnp  14015  metcnp2  14016  metcn  14017  txmetcnp  14021  txmetcn  14022  metcnpd  14023  bl2ioo  14045  addcncntoplem  14054  elcncf  14063  elcncf2  14064  ivthdec  14125  ellimc3apf  14132  cnlimcim  14143  dveflem  14190  sincosq2sgn  14251  sinq12gt0  14254  logltb  14298  ltexp2  14363  lgsdilem  14431  lgsdir2lem4  14435  lgsdir2  14437  lgsne0  14442  lgsabs1  14443  2lgsoddprmlem4  14463  2sqlem7  14471  2sqlem8a  14472  cbvrald  14543  bj-nalset  14650  bj-sels  14669  bj-nnelirr  14708  isomninnlem  14781  iswomninnlem  14800  iswomni0  14802  ismkvnnlem  14803