ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bitrd Unicode version

Theorem bitrd 187
Description: Deduction form of bitri 183. (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
StepHypRef Expression
1 bitrd.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21pm5.74i 179 . . 3  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
3 bitrd.2 . . . 4  |-  ( ph  ->  ( ch  <->  th )
)
43pm5.74i 179 . . 3  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
52, 4bitri 183 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  th ) )
65pm5.74ri 180 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bitr2d  188  bitr3d  189  bitr4d  190  syl5bb  191  syl6bb  195  3bitrd  213  3bitr2d  215  3bitr3d  217  3bitr4d  219  imbi12d  233  bibi12d  234  sylan9bb  457  anbi12d  464  orbi12d  767  con1biidc  847  pm4.54dc  872  dn1dc  929  dedlem0a  937  xorbi12d  1345  nbbndc  1357  eleq12d  2188  neeq12d  2305  neleq12d  2386  raleqbi1dv  2611  rexeqbi1dv  2612  reueqd  2613  rmoeqd  2614  raleqbidv  2615  rexeqbidv  2616  raleqbidva  2617  rexeqbidva  2618  eueq3dc  2831  sbc19.21g  2949  sbcabel  2962  sbcel1g  2992  sbceq1g  2993  sbcel2g  2994  sbceq2g  2995  sbccsb2g  3002  sbcco3g  3027  sseq12d  3098  raaanlem  3438  sbcssg  3442  ralsng  3534  2ralunsn  3695  csbunig  3714  disjeq12d  3885  breq123d  3913  sbcbr12g  3953  sbcbr1g  3954  sbcbr2g  3955  treq  4002  nalset  4028  exmidsssn  4095  copsex4g  4139  sucelon  4389  posng  4581  csbxpg  4590  sbcrel  4595  csbcnvg  4693  eliniseg  4879  brcodir  4896  csbrng  4970  sbcfung  5117  fneq12d  5185  feq12d  5232  feq123d  5233  sbcfng  5240  sbcfg  5241  f1osng  5376  csbfv12g  5425  funimass4  5440  dmfco  5457  eqfnfv  5486  eqfnfv2  5487  fneqeql2  5497  fvimacnvi  5502  funimass3  5504  fniniseg  5508  rexsupp  5512  unpreima  5513  ralrnmpt  5530  rexrnmpt  5531  dffo3  5535  fmptco  5554  fressnfv  5575  eufnfv  5616  foima2  5621  fnunirn  5636  dff13  5637  f1elima  5642  cocan1  5656  cocan2  5657  fliftel  5662  fliftf  5668  isoresbr  5678  isoini  5687  f1oiso  5695  f1ofveu  5730  mpoeq123dva  5800  ovid  5855  ov  5858  ovg  5877  ovelrn  5887  caovord2d  5908  ofrfval2  5966  offveqb  5969  eqop  6043  reldm  6052  f1od2  6100  mpoxopoveq  6105  mpoxopovel  6106  tpostpos  6129  smoiso  6167  frecabcl  6264  frecsuclem  6271  nnaordr  6374  nnaword  6375  nnaordex  6391  ereq1  6404  brdifun  6424  erth2  6442  qliftfun  6479  brecop  6487  elmapg  6523  elpmg  6526  dom2lem  6634  xpcomco  6688  php5fin  6744  elfi2  6828  supisolem  6863  inflbti  6879  inl11  6918  ismkvnex  6997  mkvprop  7000  exmidfodomrlemreseldju  7024  ltapig  7114  ltmpig  7115  nlt1pig  7117  mulcmpblnq  7144  ltsonq  7174  lt2addnq  7180  lt2mulnq  7181  archnqq  7193  prarloclemarch  7194  ltrnqg  7196  mulcmpblnq0  7220  preqlu  7248  genpdflem  7283  addnqprllem  7303  addnqprulem  7304  addlocprlemgt  7310  appdivnq  7339  mulnqprl  7344  mulnqpru  7345  mullocprlem  7346  distrlem4prl  7360  distrlem4pru  7361  1idprl  7366  1idpru  7367  ltexprlemloc  7383  cauappcvgprlemladdrl  7433  cauappcvgprlemladd  7434  cauappcvgprlem1  7435  archrecnq  7439  caucvgprlemnkj  7442  caucvgprprlemexb  7483  addcmpblnr  7515  lttrsr  7538  ltsosr  7540  ltasrg  7546  mulextsr1  7557  srpospr  7559  caucvgsrlemcau  7569  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  map2psrprg  7581  ltresr  7615  axcaucvglemres  7675  cnegexlem1  7905  negeu  7921  subadd2  7934  subcan2  7955  addrsub  8101  ltaddneg  8154  ltaddnegr  8155  ltadd1  8159  leadd2  8161  ltsubadd  8162  lesubadd  8164  ltaddsub2  8167  leaddsub2  8169  ltaddpos  8182  lesub2  8187  ltsub2  8189  ltnegcon1  8193  ltnegcon2  8194  lenegcon1  8196  lenegcon2  8197  addge01  8202  addge02  8203  suble0  8206  leaddle0  8207  lesub0  8209  eqord2  8214  sublt0d  8299  recexre  8307  reaplt  8317  reapltxor  8318  reapneg  8326  remulext1  8328  apreim  8332  apcotr  8336  apadd2  8338  addext  8339  apsub1  8371  mulcanap2d  8390  diveqap0  8409  diveqap1  8432  apmul2  8516  ltmul2  8578  lemul2  8579  ltmulgt11  8586  ltmulgt12  8587  gt0div  8592  ge0div  8593  ltmuldiv  8596  ltrec1  8610  lerec2  8611  ledivdiv  8612  ltdiv23  8614  lediv23  8615  suprleubex  8676  creur  8681  creui  8682  nn1suc  8703  nnrecl  8933  znnsub  9063  zgt0ge1  9070  zltlen  9087  nn0n0n1ge2b  9088  nn0le2is012  9091  btwnnz  9103  gtndiv  9104  prime  9108  eluz2  9288  indstr2  9359  negm  9363  nn01to3  9365  qapne  9387  qltlen  9388  qreccl  9390  divlt1lt  9466  divle1le  9467  nnledivrp  9508  xnn0xadd0  9605  xltadd2  9615  xsubge0  9619  xlesubadd  9621  iccid  9663  elioc2  9674  elico2  9675  elicc2  9676  elfz2  9752  fzen  9778  fzsubel  9795  elfzp1  9807  fzpr  9812  fzrevral2  9841  fzrevral3  9842  nn0disj  9870  2ffzeq  9873  fzosplitsni  9967  fvinim0ffz  9973  ioo0  9992  ico0  9994  ioc0  9995  modq0  10057  negqmod0  10059  zmodidfzo  10081  frecuzrdgtcl  10140  nn0ennn  10161  sq11  10320  nn0le2msqd  10420  nn0opth2d  10424  hashen  10485  zfz1isolem1  10538  zfz1iso  10539  2shfti  10558  cjap  10633  cnreim  10705  rexfiuz  10716  rexanuz2  10718  abs00ap  10789  absext  10790  sqabs  10809  abslt  10815  absle  10816  absdiflt  10819  absdifle  10820  lenegsq  10822  minmax  10956  ltmininf  10961  xrminmax  10989  xrmin1inf  10991  xrmin2inf  10992  xrltmininf  10994  xrlemininf  10995  clim  11005  clim0c  11010  climrecvg1n  11072  zsumdc  11108  fsum2dlemstep  11158  binomlem  11207  pwm1geoserap1  11232  efieq  11356  sin01bnd  11378  cos01bnd  11379  dvdsval2  11408  zdvdsdc  11426  modmulconst  11437  dvdsaddr  11449  dvdsabseq  11457  fzocongeq  11468  zeo3  11477  odd2np1  11482  oddp1d2  11499  zob  11500  oddm1d2  11501  nnoddm1d2  11519  divalgb  11534  divalgmod  11536  modremain  11538  gcdn0gt0  11578  bezoutlemstep  11597  dvdssq  11631  nn0seqcvgd  11634  algcvgblem  11642  lcmdvds  11672  lcmgcdeq  11676  coprmdvds  11685  qredeq  11689  congr  11693  isprm2  11710  isprm3  11711  prmdvdsexp  11738  prmdvdsexpb  11739  prmexpb  11741  prmfac1  11742  cncongrprm  11747  oddpwdclemxy  11758  oddpwdclemodd  11761  qnumdenbi  11781  qnumgt0  11787  hashdvds  11808  crth  11811  oddennn  11816  ctinfomlemom  11851  istopg  12077  eltg  12132  eltg2  12133  tgss2  12159  bastop1  12163  bastop2  12164  iscld  12183  isnei  12224  neiint  12225  iscn  12277  iscnp  12279  iscnp3  12283  tgcn  12288  ssidcn  12290  lmbr2  12294  lmbrf  12295  cnnei  12312  cnrest2  12316  eltx  12339  imasnopn  12379  ispsmet  12403  ismet  12424  isxmet  12425  metn0  12458  xmetres2  12459  elbl3ps  12474  elbl3  12475  xblpnfps  12478  xblpnf  12479  elmopn2  12529  metss  12574  bdxmet  12581  metrest  12586  xmetxp  12587  xmetxpbl  12588  metcnp3  12591  metcnp  12592  metcnp2  12593  metcn  12594  txmetcnp  12598  txmetcn  12599  metcnpd  12600  bl2ioo  12622  addcncntoplem  12631  elcncf  12640  elcncf2  12641  ivthdec  12702  ellimc3apf  12709  cnlimcim  12720  dveflem  12766  sincosq2sgn  12819  sinq12gt0  12822  cbvrald  12891  bj-nalset  12989  bj-sels  13008  bj-nnelirr  13047  isomninnlem  13121
  Copyright terms: Public domain W3C validator