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

Theorem imbi12d 233
Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
imbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
imbi12d  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )

Proof of Theorem imbi12d
StepHypRef Expression
1 imbi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21imbi1d 230 . 2  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43imbi2d 229 . 2  |-  ( ph  ->  ( ( ch  ->  th )  <->  ( ch  ->  ta ) ) )
52, 4bitrd 187 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )
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:  stbid  818  nfbidf  1520  drnf1  1712  drnf2  1713  equveli  1733  ax11v2  1793  ax11v  1800  ax11ev  1801  equs5or  1803  mobidh  2034  mobid  2035  axext3  2123  cbvralf  2651  cbvraldva2  2664  gencbval  2737  vtoclgaf  2754  vtocl2gaf  2756  vtocl3gaf  2758  rspct  2785  rspc  2786  rspc2gv  2804  ceqex  2815  ralab2  2851  mob2  2867  mob  2869  morex  2871  reu7  2882  reu8  2883  nelrdva  2894  cdeqim  2905  sbcimg  2953  csbhypf  3042  cbvralcsf  3066  dfss2f  3092  sbcssg  3476  sneqrg  3696  elintab  3789  intss1  3793  intmin  3798  dfiin2g  3853  disji2  3929  disjiun  3931  trel  4040  trss  4042  bnd2  4104  zfpow  4106  exmidexmid  4127  exmidsssnc  4133  exmidundifim  4137  rext  4144  opth  4166  copsexg  4173  poeq1  4228  pocl  4232  swopolem  4234  swopo  4235  soeq1  4244  sowlin  4249  frforeq2  4274  frforeq3  4276  frirrg  4279  frind  4281  weeq1  4285  ordelord  4310  reusv3i  4387  ordtriexmid  4444  ontr2exmid  4447  onsucsssucexmid  4449  onsucelsucexmid  4452  ordsucunielexmid  4453  regexmidlem1  4455  regexmid  4457  reg2exmid  4458  elirr  4463  en2lp  4476  ordsoexmid  4484  onintexmid  4494  reg3exmid  4501  tfis  4504  tfisi  4508  peano2  4516  findes  4524  nnregexmid  4541  omsinds  4542  vtoclr  4594  poinxp  4615  soinxp  4616  posng  4618  ssrel  4634  ssrel2  4636  ssrelrel  4646  relop  4696  issref  4928  iota5  5115  dffun4f  5146  sbcfung  5154  funopg  5164  brprcneu  5421  funfveu  5441  tz6.12f  5457  funbrfv  5467  ssimaexg  5490  fvmptss2  5503  fvmptssdm  5512  fvmptf  5520  fvelrn  5558  f1veqaeq  5677  dff13f  5678  isopolem  5730  isosolem  5732  riota5f  5761  imbrov2fvoveq  5806  oprabid  5810  ovmpos  5901  ov2gf  5902  ovi3  5914  caovcan  5942  caovordig  5943  caofrss  6013  caoftrn  6014  dfoprab4f  6098  f1o2ndf1  6132  poxp  6136  smoel  6204  tfrlem1  6212  tfr1onlemsucfn  6244  tfr1onlemsucaccv  6245  tfr1onlembxssdm  6247  tfr1onlembfn  6248  tfr1onlemaccex  6252  tfr1onlemres  6253  tfrcllemsucfn  6257  tfrcllemsucaccv  6258  tfrcllembxssdm  6260  tfrcllembfn  6261  tfrcllemaccex  6265  tfrcllemres  6266  tfrcl  6268  nnsucelsuc  6394  nnsucsssuc  6395  nnmordi  6419  nnaordex  6430  qsel  6513  eroveu  6527  ecopovtrn  6533  ecopovtrng  6536  th3qlem2  6539  ixpsnf1o  6637  fundmeng  6708  phplem3g  6757  nneneq  6758  ssfiexmid  6777  domfiexmid  6779  findcard  6789  findcard2  6790  findcard2s  6791  findcard2d  6792  findcard2sd  6793  diffifi  6795  ac6sfi  6799  fiintim  6824  fisseneq  6827  fidcenumlemrk  6849  fidcenumlemr  6850  isbth  6862  supeq3  6884  supeq123d  6885  supmoti  6887  suplubti  6894  supisolem  6902  cnvinfex  6912  eqinfti  6914  infvalti  6916  ordiso2  6927  isomni  7015  finomni  7019  exmidomni  7021  ctssexmid  7031  ismkv  7034  ismkvnex  7036  mkvprop  7039  fodjumkvlemres  7040  enmkvlem  7042  iswomni  7046  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  ccfunen  7095  ltsonq  7229  ltexnqq  7239  prcdnql  7315  prcunqu  7316  prloc  7322  prdisj  7323  genprndl  7352  genprndu  7353  caucvgprlemnkj  7497  caucvgprlemnbj  7498  caucvgprlemcl  7507  caucvgprprlemcbv  7518  caucvgprprlemval  7519  suplocexprlemloc  7552  lttrsr  7593  ltsosr  7595  recexgt0sr  7604  mulgt0sr  7609  aptisr  7610  mulextsr1  7612  srpospr  7614  caucvgsrlemgt1  7626  caucvgsrlemoffres  7631  caucvgsr  7633  map2psrprg  7636  suplocsrlemb  7637  axprecex  7711  axpre-ltwlin  7714  axpre-lttrn  7715  axpre-apti  7716  axpre-mulgt0  7718  axpre-mulext  7719  axcaucvglemcau  7729  axcaucvglemres  7730  axpre-suploclemres  7732  axpre-suploc  7733  axsuploc  7860  ltleletr  7869  ltordlem  8267  squeeze0  8685  sup3exmid  8738  nnsub  8782  fzind  9189  uzind4s  9411  uzind4s2  9412  indstr  9414  supinfneg  9416  infsupneg  9417  frec2uzuzd  10205  frec2uzltd  10206  uzsinds  10245  seq3fveq2  10272  seq3shft2  10276  monoord  10279  seq3split  10282  seq3id2  10312  expcl2lemap  10335  facdiv  10515  facwordi  10517  zfz1isolem1  10614  zfz1iso  10615  seq3coll  10616  caucvgre  10784  fimaxre2  11029  climcn1  11108  climcn2  11109  subcn2  11111  summodclem2a  11181  fsumsplitf  11208  fsum2d  11235  modfsummod  11258  fsumabs  11265  telfsumo  11266  fsumiun  11277  prodfdivap  11347  ndvdssub  11661  bezoutlemmain  11720  bezoutlemex  11723  bezoutlemzz  11724  bezoutlemsup  11731  dfgcd2  11736  algcvg  11763  algcvga  11766  algfx  11767  lcmgcdlem  11792  lcmdvds  11794  coprmgcdb  11803  coprmdvds1  11806  coprmdvds2  11808  prmind2  11835  dvdsprime  11837  nprm  11838  dvdsprm  11851  exprmfct  11852  coprm  11856  isprm6  11859  prmfac1  11864  sqrt2irr  11874  ennnfonelemim  11971  exmidunben  11973  uniopn  12205  fiinopn  12208  epttop  12296  cnpval  12404  iscnp  12405  icnpimaex  12417  lmcvg  12423  cnptoprest  12445  cnptoprest2  12446  lmss  12452  lmff  12455  txcnp  12477  txlm  12485  cnmpt12  12493  cnmpt22  12500  blssps  12633  blss  12634  metss  12700  comet  12705  metcnp3  12717  metcnp2  12719  txmetcnp  12724  divcnap  12761  elcncf2  12767  cncfi  12771  mulc1cncf  12782  cncfmet  12785  mulcncflem  12796  mulcncf  12797  dedekindeulemloc  12803  dedekindeulemlu  12805  dedekindeulemeu  12806  suplociccreex  12808  dedekindicclemloc  12812  dedekindicclemlu  12814  dedekindicclemeu  12815  ivthinclemlopn  12820  ivthinclemlr  12821  ivthinclemuopn  12822  ivthinclemur  12823  ivthinclemloc  12825  limccl  12834  ellimc3apf  12835  limccnpcntop  12850  limccnp2lem  12851  limccoap  12853  dvcoapbr  12877  cbvrald  13164  bj-bdfindes  13316  bj-omtrans  13323  bj-inf2vnlem1  13337  bj-inf2vnlem2  13338  bj-inf2vnlem3  13339  bj-inf2vnlem4  13340  bj-findes  13348  strcoll2  13350  sscoll2  13355  exmid1stab  13366  subctctexmid  13367  pw1nct  13369  exmidsbthrlem  13390  sbthom  13394  apdiff  13414  ismkvnnlem  13417  neapmkv  13423
  Copyright terms: Public domain W3C validator