ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi12d GIF 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 (𝜑 → (𝜓𝜒))
imbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
imbi12d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))

Proof of Theorem imbi12d
StepHypRef Expression
1 imbi12d.1 . . 3 (𝜑 → (𝜓𝜒))
21imbi1d 230 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43imbi2d 229 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 187 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
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  802  nfbidf  1504  drnf1  1696  drnf2  1697  equveli  1717  ax11v2  1776  ax11v  1783  ax11ev  1784  equs5or  1786  mobidh  2011  mobid  2012  axext3  2100  cbvralf  2625  cbvraldva2  2635  gencbval  2708  vtoclgaf  2725  vtocl2gaf  2727  vtocl3gaf  2729  rspct  2756  rspc  2757  rspc2gv  2775  ceqex  2786  ralab2  2821  mob2  2837  mob  2839  morex  2841  reu7  2852  reu8  2853  nelrdva  2864  cdeqim  2875  sbcimg  2922  csbhypf  3008  cbvralcsf  3032  dfss2f  3058  sbcssg  3442  sneqrg  3659  elintab  3752  intss1  3756  intmin  3761  dfiin2g  3816  disji2  3892  disjiun  3894  trel  4003  trss  4005  bnd2  4067  zfpow  4069  exmidexmid  4090  exmidsssnc  4096  exmidundifim  4100  rext  4107  opth  4129  copsexg  4136  poeq1  4191  pocl  4195  swopolem  4197  swopo  4198  soeq1  4207  sowlin  4212  frforeq2  4237  frforeq3  4239  frirrg  4242  frind  4244  weeq1  4248  ordelord  4273  reusv3i  4350  ordtriexmid  4407  ontr2exmid  4410  onsucsssucexmid  4412  onsucelsucexmid  4415  ordsucunielexmid  4416  regexmidlem1  4418  regexmid  4420  reg2exmid  4421  elirr  4426  en2lp  4439  ordsoexmid  4447  onintexmid  4457  reg3exmid  4464  tfis  4467  tfisi  4471  peano2  4479  findes  4487  nnregexmid  4504  omsinds  4505  vtoclr  4557  poinxp  4578  soinxp  4579  posng  4581  ssrel  4597  ssrel2  4599  ssrelrel  4609  relop  4659  issref  4891  iota5  5078  dffun4f  5109  sbcfung  5117  funopg  5127  brprcneu  5382  funfveu  5402  tz6.12f  5418  funbrfv  5428  ssimaexg  5451  fvmptss2  5464  fvmptssdm  5473  fvmptf  5481  fvelrn  5519  f1veqaeq  5638  dff13f  5639  isopolem  5691  isosolem  5693  riota5f  5722  imbrov2fvoveq  5767  oprabid  5771  ovmpos  5862  ov2gf  5863  ovi3  5875  caovcan  5903  caovordig  5904  caofrss  5974  caoftrn  5975  dfoprab4f  6059  f1o2ndf1  6093  poxp  6097  smoel  6165  tfrlem1  6173  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemaccex  6213  tfr1onlemres  6214  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemaccex  6226  tfrcllemres  6227  tfrcl  6229  nnsucelsuc  6355  nnsucsssuc  6356  nnmordi  6380  nnaordex  6391  qsel  6474  eroveu  6488  ecopovtrn  6494  ecopovtrng  6497  th3qlem2  6500  ixpsnf1o  6598  fundmeng  6669  phplem3g  6718  nneneq  6719  ssfiexmid  6738  domfiexmid  6740  findcard  6750  findcard2  6751  findcard2s  6752  findcard2d  6753  findcard2sd  6754  diffifi  6756  ac6sfi  6760  fiintim  6785  fisseneq  6788  fidcenumlemrk  6810  fidcenumlemr  6811  isbth  6823  supeq3  6845  supeq123d  6846  supmoti  6848  suplubti  6855  supisolem  6863  cnvinfex  6873  eqinfti  6875  infvalti  6877  ordiso2  6888  isomni  6976  finomni  6980  exmidomni  6982  ctssexmid  6992  ismkv  6995  ismkvnex  6997  mkvprop  7000  fodjumkvlemres  7001  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  ccfunen  7047  ltsonq  7174  ltexnqq  7184  prcdnql  7260  prcunqu  7261  prloc  7267  prdisj  7268  genprndl  7297  genprndu  7298  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemcl  7452  caucvgprprlemcbv  7463  caucvgprprlemval  7464  suplocexprlemloc  7497  lttrsr  7538  ltsosr  7540  recexgt0sr  7549  mulgt0sr  7554  aptisr  7555  mulextsr1  7557  srpospr  7559  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  caucvgsr  7578  map2psrprg  7581  suplocsrlemb  7582  axprecex  7656  axpre-ltwlin  7659  axpre-lttrn  7660  axpre-apti  7661  axpre-mulgt0  7663  axpre-mulext  7664  axcaucvglemcau  7674  axcaucvglemres  7675  axpre-suploclemres  7677  axpre-suploc  7678  axsuploc  7805  ltleletr  7814  ltordlem  8212  squeeze0  8626  sup3exmid  8679  nnsub  8723  fzind  9124  uzind4s  9341  uzind4s2  9342  indstr  9344  supinfneg  9346  infsupneg  9347  frec2uzuzd  10130  frec2uzltd  10131  uzsinds  10170  seq3fveq2  10197  seq3shft2  10201  monoord  10204  seq3split  10207  seq3id2  10237  expcl2lemap  10260  facdiv  10439  facwordi  10441  zfz1isolem1  10538  zfz1iso  10539  seq3coll  10540  caucvgre  10708  fimaxre2  10953  climcn1  11032  climcn2  11033  subcn2  11035  summodclem2a  11105  fsumsplitf  11132  fsum2d  11159  modfsummod  11182  fsumabs  11189  telfsumo  11190  fsumiun  11201  ndvdssub  11539  bezoutlemmain  11598  bezoutlemex  11601  bezoutlemzz  11602  bezoutlemsup  11609  dfgcd2  11614  algcvg  11641  algcvga  11644  algfx  11645  lcmgcdlem  11670  lcmdvds  11672  coprmgcdb  11681  coprmdvds1  11684  coprmdvds2  11686  prmind2  11713  dvdsprime  11715  nprm  11716  dvdsprm  11729  exprmfct  11730  coprm  11734  isprm6  11737  prmfac1  11742  sqrt2irr  11752  ennnfonelemim  11848  exmidunben  11850  uniopn  12079  fiinopn  12082  epttop  12170  cnpval  12278  iscnp  12279  icnpimaex  12291  lmcvg  12297  cnptoprest  12319  cnptoprest2  12320  lmss  12326  lmff  12329  txcnp  12351  txlm  12359  cnmpt12  12367  cnmpt22  12374  blssps  12507  blss  12508  metss  12574  comet  12579  metcnp3  12591  metcnp2  12593  txmetcnp  12598  divcnap  12635  elcncf2  12641  cncfi  12645  mulc1cncf  12656  cncfmet  12659  mulcncflem  12670  mulcncf  12671  dedekindeulemloc  12677  dedekindeulemlu  12679  dedekindeulemeu  12680  suplociccreex  12682  dedekindicclemloc  12686  dedekindicclemlu  12688  dedekindicclemeu  12689  ivthinclemlopn  12694  ivthinclemlr  12695  ivthinclemuopn  12696  ivthinclemur  12697  ivthinclemloc  12699  limccl  12708  ellimc3apf  12709  limccnpcntop  12724  limccnp2lem  12725  limccoap  12727  dvcoapbr  12751  cbvrald  12891  bj-bdfindes  13043  bj-omtrans  13050  bj-inf2vnlem1  13064  bj-inf2vnlem2  13065  bj-inf2vnlem3  13066  bj-inf2vnlem4  13067  bj-findes  13075  strcoll2  13077  sscoll2  13082  exmid1stab  13091  subctctexmid  13092  exmidsbthrlem  13113  sbthom  13117
  Copyright terms: Public domain W3C validator