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  455  anbi12d  462  orbi12d  765  con1biidc  845  pm4.54dc  870  dn1dc  927  dedlem0a  935  xorbi12d  1343  nbbndc  1355  eleq12d  2186  neeq12d  2303  neleq12d  2384  raleqbi1dv  2609  rexeqbi1dv  2610  reueqd  2611  rmoeqd  2612  raleqbidv  2613  rexeqbidv  2614  raleqbidva  2615  rexeqbidva  2616  eueq3dc  2829  sbc19.21g  2947  sbcabel  2960  sbcel1g  2990  sbceq1g  2991  sbcel2g  2992  sbceq2g  2993  sbccsb2g  3000  sbcco3g  3025  sseq12d  3096  raaanlem  3436  sbcssg  3440  ralsng  3532  2ralunsn  3693  csbunig  3712  disjeq12d  3883  breq123d  3911  sbcbr12g  3951  sbcbr1g  3952  sbcbr2g  3953  treq  4000  nalset  4026  exmidsssn  4093  copsex4g  4137  sucelon  4387  posng  4579  csbxpg  4588  sbcrel  4593  csbcnvg  4691  eliniseg  4877  brcodir  4894  csbrng  4968  sbcfung  5115  fneq12d  5183  feq12d  5230  feq123d  5231  sbcfng  5238  sbcfg  5239  f1osng  5374  csbfv12g  5423  funimass4  5438  dmfco  5455  eqfnfv  5484  eqfnfv2  5485  fneqeql2  5495  fvimacnvi  5500  funimass3  5502  fniniseg  5506  rexsupp  5510  unpreima  5511  ralrnmpt  5528  rexrnmpt  5529  dffo3  5533  fmptco  5552  fressnfv  5573  eufnfv  5614  foima2  5619  fnunirn  5634  dff13  5635  f1elima  5640  cocan1  5654  cocan2  5655  fliftel  5660  fliftf  5666  isoresbr  5676  isoini  5685  f1oiso  5693  f1ofveu  5728  mpoeq123dva  5798  ovid  5853  ov  5856  ovg  5875  ovelrn  5885  caovord2d  5906  ofrfval2  5964  offveqb  5967  eqop  6041  reldm  6050  f1od2  6098  mpoxopoveq  6103  mpoxopovel  6104  tpostpos  6127  smoiso  6165  frecabcl  6262  frecsuclem  6269  nnaordr  6372  nnaword  6373  nnaordex  6389  ereq1  6402  brdifun  6422  erth2  6440  qliftfun  6477  brecop  6485  elmapg  6521  elpmg  6524  dom2lem  6632  xpcomco  6686  php5fin  6742  elfi2  6826  supisolem  6861  inflbti  6877  inl11  6916  ismkvnex  6995  mkvprop  6998  exmidfodomrlemreseldju  7020  ltapig  7110  ltmpig  7111  nlt1pig  7113  mulcmpblnq  7140  ltsonq  7170  lt2addnq  7176  lt2mulnq  7177  archnqq  7189  prarloclemarch  7190  ltrnqg  7192  mulcmpblnq0  7216  preqlu  7244  genpdflem  7279  addnqprllem  7299  addnqprulem  7300  addlocprlemgt  7306  appdivnq  7335  mulnqprl  7340  mulnqpru  7341  mullocprlem  7342  distrlem4prl  7356  distrlem4pru  7357  1idprl  7362  1idpru  7363  ltexprlemloc  7379  cauappcvgprlemladdrl  7429  cauappcvgprlemladd  7430  cauappcvgprlem1  7431  archrecnq  7435  caucvgprlemnkj  7438  caucvgprprlemexb  7479  addcmpblnr  7511  lttrsr  7534  ltsosr  7536  ltasrg  7542  mulextsr1  7553  srpospr  7555  caucvgsrlemcau  7565  caucvgsrlemgt1  7567  caucvgsrlemoffres  7572  map2psrprg  7577  ltresr  7611  axcaucvglemres  7671  cnegexlem1  7901  negeu  7917  subadd2  7930  subcan2  7951  addrsub  8097  ltaddneg  8150  ltaddnegr  8151  ltadd1  8155  leadd2  8157  ltsubadd  8158  lesubadd  8160  ltaddsub2  8163  leaddsub2  8165  ltaddpos  8178  lesub2  8183  ltsub2  8185  ltnegcon1  8189  ltnegcon2  8190  lenegcon1  8192  lenegcon2  8193  addge01  8198  addge02  8199  suble0  8202  leaddle0  8203  lesub0  8205  eqord2  8210  sublt0d  8295  recexre  8303  reaplt  8313  reapltxor  8314  reapneg  8322  remulext1  8324  apreim  8328  apcotr  8332  apadd2  8334  addext  8335  apsub1  8366  mulcanap2d  8383  diveqap0  8402  diveqap1  8425  apmul2  8509  ltmul2  8571  lemul2  8572  ltmulgt11  8579  ltmulgt12  8580  gt0div  8585  ge0div  8586  ltmuldiv  8589  ltrec1  8603  lerec2  8604  ledivdiv  8605  ltdiv23  8607  lediv23  8608  suprleubex  8669  creur  8674  creui  8675  nn1suc  8696  nnrecl  8926  znnsub  9056  zgt0ge1  9063  zltlen  9080  nn0n0n1ge2b  9081  nn0le2is012  9084  btwnnz  9096  gtndiv  9097  prime  9101  eluz2  9281  indstr2  9352  negm  9356  nn01to3  9358  qapne  9380  qltlen  9381  qreccl  9383  divlt1lt  9457  divle1le  9458  nnledivrp  9493  xnn0xadd0  9590  xltadd2  9600  xsubge0  9604  xlesubadd  9606  iccid  9648  elioc2  9659  elico2  9660  elicc2  9661  elfz2  9737  fzen  9763  fzsubel  9780  elfzp1  9792  fzpr  9797  fzrevral2  9826  fzrevral3  9827  nn0disj  9855  2ffzeq  9858  fzosplitsni  9952  fvinim0ffz  9958  ioo0  9977  ico0  9979  ioc0  9980  modq0  10042  negqmod0  10044  zmodidfzo  10066  frecuzrdgtcl  10125  nn0ennn  10146  sq11  10305  nn0le2msqd  10405  nn0opth2d  10409  hashen  10470  zfz1isolem1  10523  zfz1iso  10524  2shfti  10543  cjap  10618  cnreim  10690  rexfiuz  10701  rexanuz2  10703  abs00ap  10774  absext  10775  sqabs  10794  abslt  10800  absle  10801  absdiflt  10804  absdifle  10805  lenegsq  10807  minmax  10941  ltmininf  10946  xrminmax  10974  xrmin1inf  10976  xrmin2inf  10977  xrltmininf  10979  xrlemininf  10980  clim  10990  clim0c  10995  climrecvg1n  11057  zsumdc  11093  fsum2dlemstep  11143  binomlem  11192  pwm1geoserap1  11217  efieq  11341  sin01bnd  11363  cos01bnd  11364  dvdsval2  11392  zdvdsdc  11410  modmulconst  11421  dvdsaddr  11433  dvdsabseq  11441  fzocongeq  11452  zeo3  11461  odd2np1  11466  oddp1d2  11483  zob  11484  oddm1d2  11485  nnoddm1d2  11503  divalgb  11518  divalgmod  11520  modremain  11522  gcdn0gt0  11562  bezoutlemstep  11581  dvdssq  11615  nn0seqcvgd  11618  algcvgblem  11626  lcmdvds  11656  lcmgcdeq  11660  coprmdvds  11669  qredeq  11673  congr  11677  isprm2  11694  isprm3  11695  prmdvdsexp  11722  prmdvdsexpb  11723  prmexpb  11725  prmfac1  11726  cncongrprm  11731  oddpwdclemxy  11742  oddpwdclemodd  11745  qnumdenbi  11765  qnumgt0  11771  hashdvds  11792  crth  11795  oddennn  11800  ctinfomlemom  11835  istopg  12061  eltg  12116  eltg2  12117  tgss2  12143  bastop1  12147  bastop2  12148  iscld  12167  isnei  12208  neiint  12209  iscn  12261  iscnp  12263  iscnp3  12267  tgcn  12272  ssidcn  12274  lmbr2  12278  lmbrf  12279  cnnei  12296  cnrest2  12300  eltx  12323  imasnopn  12363  ispsmet  12387  ismet  12408  isxmet  12409  metn0  12442  xmetres2  12443  elbl3ps  12458  elbl3  12459  xblpnfps  12462  xblpnf  12463  elmopn2  12513  metss  12558  bdxmet  12565  metrest  12570  xmetxp  12571  xmetxpbl  12572  metcnp3  12575  metcnp  12576  metcnp2  12577  metcn  12578  txmetcnp  12582  txmetcn  12583  metcnpd  12584  bl2ioo  12606  addcncntoplem  12615  elcncf  12624  elcncf2  12625  ellimc3apf  12681  cnlimcim  12692  dveflem  12738  cbvrald  12806  bj-nalset  12904  bj-sels  12923  bj-nnelirr  12962  isomninnlem  13036
  Copyright terms: Public domain W3C validator