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  795  con1biidc  879  pm4.54dc  904  dn1dc  963  dedlem0a  971  3bior2fd  1366  xorbi12d  1402  nbbndc  1414  eleq12d  2276  neeq12d  2396  neleq12d  2477  raleqbi1dv  2714  rexeqbi1dv  2715  reueqd  2716  rmoeqd  2717  raleqbidv  2718  rexeqbidv  2719  raleqbidva  2720  rexeqbidva  2721  eueq3dc  2947  sbc19.21g  3067  sbcabel  3080  sbcel1g  3112  sbceq1g  3113  sbcel2g  3114  sbceq2g  3115  sbccsb2g  3123  sbcco3g  3151  sseq12d  3224  raaanlem  3565  sbcssg  3569  ralsng  3673  2ralunsn  3839  csbunig  3858  disjeq12d  4030  breq123d  4058  sbcbr12g  4099  sbcbr1g  4100  sbcbr2g  4101  treq  4148  nalset  4174  exmidsssn  4246  copsex4g  4291  onsucb  4551  posng  4747  csbxpg  4756  sbcrel  4761  csbcnvg  4862  eliniseg  5052  brcodir  5070  csbrng  5144  sbcfung  5295  fneq12d  5366  feq12d  5415  feq123d  5416  sbcfng  5423  sbcfg  5424  f1osng  5563  csbfv12g  5614  funimass4  5629  dmfco  5647  eqfnfv  5677  eqfnfv2  5678  fneqeql2  5689  fvimacnvi  5694  funimass3  5696  fniniseg  5700  rexsupp  5704  unpreima  5705  ralrnmpt  5722  rexrnmpt  5723  dffo3  5727  fmptco  5746  fressnfv  5771  eufnfv  5815  foima2  5820  fnunirn  5836  dff13  5837  f1elima  5842  cocan1  5856  cocan2  5857  fliftel  5862  fliftf  5868  isoresbr  5878  isoini  5887  f1oiso  5895  f1ofveu  5932  mpoeq123dva  6006  ovid  6062  ov  6065  ovg  6085  ovelrn  6095  caovord2d  6116  ofrfval2  6175  offveqb  6178  eqop  6263  reldm  6272  f1od2  6321  mpoxopoveq  6326  mpoxopovel  6327  tpostpos  6350  smoiso  6388  frecabcl  6485  frecsuclem  6492  nnaordr  6596  nnaword  6597  nnaordex  6614  ereq1  6627  brdifun  6647  erth2  6667  qliftfun  6704  brecop  6712  elmapg  6748  elpmg  6751  dom2lem  6863  xpcomco  6921  pw2f1odclem  6931  php5fin  6979  elfi2  7074  supisolem  7110  inflbti  7126  inl11  7167  ismkvnex  7257  mkvprop  7260  nninfwlporlemd  7274  exmidfodomrlemreseldju  7308  ltapig  7451  ltmpig  7452  nlt1pig  7454  mulcmpblnq  7481  ltsonq  7511  lt2addnq  7517  lt2mulnq  7518  archnqq  7530  prarloclemarch  7531  ltrnqg  7533  mulcmpblnq0  7557  preqlu  7585  genpdflem  7620  addnqprllem  7640  addnqprulem  7641  addlocprlemgt  7647  appdivnq  7676  mulnqprl  7681  mulnqpru  7682  mullocprlem  7683  distrlem4prl  7697  distrlem4pru  7698  1idprl  7703  1idpru  7704  ltexprlemloc  7720  cauappcvgprlemladdrl  7770  cauappcvgprlemladd  7771  cauappcvgprlem1  7772  archrecnq  7776  caucvgprlemnkj  7779  caucvgprprlemexb  7820  addcmpblnr  7852  lttrsr  7875  ltsosr  7877  ltasrg  7883  mulextsr1  7894  srpospr  7896  caucvgsrlemcau  7906  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  map2psrprg  7918  ltresr  7952  axcaucvglemres  8012  eqlelt  8159  cnegexlem1  8247  negeu  8263  subadd2  8276  subcan2  8297  addrsub  8443  ltaddneg  8497  ltaddnegr  8498  ltadd1  8502  leadd2  8504  ltsubadd  8505  lesubadd  8507  ltaddsub2  8510  leaddsub2  8512  ltaddpos  8525  lesub2  8530  ltsub2  8532  ltnegcon1  8536  ltnegcon2  8537  lenegcon1  8539  lenegcon2  8540  addge01  8545  addge02  8546  suble0  8549  leaddle0  8550  lesub0  8552  eqord2  8557  sublt0d  8643  recexre  8651  reaplt  8661  reapltxor  8662  reapneg  8670  remulext1  8672  apreim  8676  apcotr  8680  apadd2  8682  addext  8683  apsub1  8715  mulcanap2d  8735  diveqap0  8755  diveqap1  8778  apmul2  8862  ltmul2  8929  lemul2  8930  ltmulgt11  8937  ltmulgt12  8938  gt0div  8943  ge0div  8944  ltmuldiv  8947  ltrec1  8961  lerec2  8962  ledivdiv  8963  ltdiv23  8965  lediv23  8966  suprleubex  9027  creur  9032  creui  9033  nn1suc  9055  nnrecl  9293  znnsub  9424  zgt0ge1  9431  zltlen  9451  nn0n0n1ge2b  9452  nn0le2is012  9455  btwnnz  9467  gtndiv  9468  prime  9472  eluz2  9654  indstr2  9730  negm  9736  nn01to3  9738  qapne  9760  qltlen  9761  qreccl  9763  irrmulap  9769  divlt1lt  9846  divle1le  9847  nnledivrp  9888  xnn0xadd0  9989  xltadd2  9999  xsubge0  10003  xlesubadd  10005  iccid  10047  elioc2  10058  elico2  10059  elicc2  10060  elfz2  10137  fzen  10165  fzsubel  10182  elfzp1  10194  fzpr  10199  fzrevral2  10228  fzrevral3  10229  nn0disj  10260  2ffzeq  10263  fzosplitsni  10364  fvinim0ffz  10370  ioo0  10402  ico0  10404  ioc0  10405  modq0  10474  negqmod0  10476  zmodidfzo  10498  frecuzrdgtcl  10557  nn0ennn  10578  nninfinf  10588  sq11  10757  nn0le2msqd  10864  nn0opth2d  10868  hashen  10929  zfz1isolem1  10985  zfz1iso  10986  csbwrdg  11023  wrdnval  11024  eqwrd  11034  ccat0  11052  ccatws1lenp1bg  11089  swrd0g  11113  swrdspsleq  11120  2shfti  11142  cjap  11217  cnreim  11289  rexfiuz  11300  rexanuz2  11302  abs00ap  11373  absext  11374  sqabs  11393  abslt  11399  absle  11400  absdiflt  11403  absdifle  11404  lenegsq  11406  minmax  11541  ltmininf  11546  mingeb  11553  xrminmax  11576  xrmin1inf  11578  xrmin2inf  11579  xrltmininf  11581  xrlemininf  11582  clim  11592  clim0c  11597  climrecvg1n  11659  zsumdc  11695  fsum2dlemstep  11745  binomlem  11794  pwm1geoserap1  11819  zproddc  11890  efieq  12046  sin01bnd  12068  cos01bnd  12069  dvdsval2  12101  modm1div  12111  zdvdsdc  12123  modmulconst  12134  dvdsaddr  12148  dvdsabseq  12158  fzocongeq  12169  zeo3  12179  odd2np1  12184  oddp1d2  12201  zob  12202  oddm1d2  12203  nnoddm1d2  12221  divalgb  12236  divalgmod  12238  modremain  12240  bits0  12259  bitsp1e  12263  bitsp1o  12264  bitscmp  12269  bitsinv1lem  12272  gcdn0gt0  12299  bezoutlemstep  12318  dvdssq  12352  nn0seqcvgd  12363  algcvgblem  12371  lcmdvds  12401  lcmgcdeq  12405  coprmdvds  12414  qredeq  12418  congr  12422  isprm2  12439  isprm3  12440  prmdvdsexp  12470  prmdvdsexpb  12471  prmexpb  12473  prmfac1  12474  cncongrprm  12479  oddpwdclemxy  12491  oddpwdclemodd  12494  qnumdenbi  12514  qnumgt0  12520  hashdvds  12543  crth  12546  fermltl  12556  modprminveq  12573  pcpremul  12616  pc2dvds  12653  pcz  12655  prmpwdvds  12678  4sqlem16  12729  oddennn  12763  ctinfomlemom  12798  prdsbasmpt  13112  prdsbasmpt2  13120  mgm1  13202  ismhm  13293  mhmpropd  13298  issubm  13304  issubm2  13305  grpsubrcan  13413  grplactcnv  13434  grp1  13438  eqgval  13559  eqgid  13562  quselbasg  13566  isghm  13579  conjnmzb  13616  iscmn  13629  eqgabl  13666  rngmneg1  13709  rngmneg2  13710  rngpropd  13717  srgen1zr  13750  ringideu  13779  ringpropd  13800  crngpropd  13801  dvdsrd  13856  dvdsr02  13867  opprunitd  13872  crngunit  13873  unitpropdg  13910  rhmunitinv  13940  isnzr2  13946  issubrng  13961  resrhm2b  14011  aprval  14044  islmod  14053  islssm  14119  islssmg  14120  ellspsn  14179  isridl  14266  zrhrhmb  14384  zndvds  14411  znleval  14415  istopg  14471  eltg  14524  eltg2  14525  tgss2  14551  bastop1  14555  bastop2  14556  iscld  14575  isnei  14616  neiint  14617  iscn  14669  iscnp  14671  iscnp3  14675  tgcn  14680  ssidcn  14682  lmbr2  14686  lmbrf  14687  cnnei  14704  cnrest2  14708  eltx  14731  imasnopn  14771  ispsmet  14795  ismet  14816  isxmet  14817  metn0  14850  xmetres2  14851  elbl3ps  14866  elbl3  14867  xblpnfps  14870  xblpnf  14871  elmopn2  14921  metss  14966  bdxmet  14973  metrest  14978  xmetxp  14979  xmetxpbl  14980  metcnp3  14983  metcnp  14984  metcnp2  14985  metcn  14986  txmetcnp  14990  txmetcn  14991  metcnpd  14992  bl2ioo  15022  addcncntoplem  15033  elcncf  15045  elcncf2  15046  ivthdec  15116  ellimc3apf  15132  cnlimcim  15143  dveflem  15198  ply1termlem  15214  sincosq2sgn  15299  sinq12gt0  15302  logltb  15346  ltexp2  15413  wilthlem1  15452  lgsdilem  15504  lgsdir2lem4  15508  lgsdir2  15510  lgsne0  15515  lgsabs1  15516  gausslemma2dlem3  15540  gausslemma2dlem7  15545  lgseisenlem3  15549  lgsquad3  15561  2lgslem1a  15565  2lgslem3c  15572  2lgslem3d  15573  2lgsoddprmlem4  15589  2sqlem7  15598  2sqlem8a  15599  cbvrald  15724  bj-nalset  15831  bj-sels  15850  bj-nnelirr  15889  isomninnlem  15969  iswomninnlem  15988  iswomni0  15990  ismkvnnlem  15991