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

Theorem imbi12d 234
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 231 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43imbi2d 230 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 188 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff set class
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:  stbid  832  nfbidf  1539  drnf1  1733  drnf2  1734  equveli  1759  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  mobidh  2060  mobid  2061  axext3  2160  cbvralfw  2694  cbvralf  2696  cbvralvw  2707  cbvraldva2  2710  gencbval  2785  vtoclgaf  2802  vtocl2gaf  2804  vtocl3gaf  2806  rspct  2834  rspc  2835  rspc2gv  2853  ceqex  2864  ralab2  2901  mob2  2917  mob  2919  morex  2921  reu7  2932  reu8  2933  nelrdva  2944  cdeqim  2955  sbcimg  3004  csbhypf  3095  cbvralcsf  3119  dfss2f  3146  sbcssg  3532  sneqrg  3760  elintab  3853  intss1  3857  intmin  3862  dfiin2g  3917  disji2  3993  disjiun  3995  trel  4105  trss  4107  bnd2  4170  zfpow  4172  exmidexmid  4193  exmidsssnc  4200  exmidundifim  4204  exmid1stab  4205  rext  4212  opth  4234  copsexg  4241  poeq1  4296  pocl  4300  swopolem  4302  swopo  4303  soeq1  4312  sowlin  4317  frforeq2  4342  frforeq3  4344  frirrg  4347  frind  4349  weeq1  4353  ordelord  4378  reusv3i  4456  ordtriexmid  4517  ontr2exmid  4521  onsucsssucexmid  4523  onsucelsucexmid  4526  ordsucunielexmid  4527  regexmidlem1  4529  regexmid  4531  reg2exmid  4532  elirr  4537  en2lp  4550  ordsoexmid  4558  onintexmid  4569  reg3exmid  4576  tfis  4579  tfisi  4583  peano2  4591  findes  4599  nnregexmid  4617  omsinds  4618  vtoclr  4671  poinxp  4692  soinxp  4693  posng  4695  ssrel  4711  ssrel2  4713  ssrelrel  4723  relop  4773  issref  5007  iota5  5194  dffun4f  5228  sbcfung  5236  funopg  5246  brprcneu  5504  funfveu  5524  tz6.12f  5540  funbrfv  5550  ssimaexg  5574  fvmptss2  5587  fvmptssdm  5596  fvmptf  5604  fvelrn  5643  f1veqaeq  5764  dff13f  5765  isopolem  5817  isosolem  5819  riota5f  5849  imbrov2fvoveq  5894  oprabid  5901  ovmpos  5992  ov2gf  5993  ovi3  6005  caovcan  6033  caovordig  6034  caofrss  6101  caoftrn  6102  dfoprab4f  6188  f1o2ndf1  6223  poxp  6227  smoel  6295  tfrlem1  6303  tfr1onlemsucfn  6335  tfr1onlemsucaccv  6336  tfr1onlembxssdm  6338  tfr1onlembfn  6339  tfr1onlemaccex  6343  tfr1onlemres  6344  tfrcllemsucfn  6348  tfrcllemsucaccv  6349  tfrcllembxssdm  6351  tfrcllembfn  6352  tfrcllemaccex  6356  tfrcllemres  6357  tfrcl  6359  nnsucelsuc  6486  nnsucsssuc  6487  nnmordi  6511  nnaordex  6523  qsel  6606  eroveu  6620  ecopovtrn  6626  ecopovtrng  6629  th3qlem2  6632  ixpsnf1o  6730  fundmeng  6801  phplem3g  6850  nneneq  6851  ssfiexmid  6870  domfiexmid  6872  findcard  6882  findcard2  6883  findcard2s  6884  findcard2d  6885  findcard2sd  6886  diffifi  6888  ac6sfi  6892  fiintim  6922  fisseneq  6925  fidcenumlemrk  6947  fidcenumlemr  6948  isbth  6960  supeq3  6983  supeq123d  6984  supmoti  6986  suplubti  6993  supisolem  7001  cnvinfex  7011  eqinfti  7013  infvalti  7015  ordiso2  7028  nnnninfeq2  7121  isomni  7128  finomni  7132  exmidomni  7134  ctssexmid  7142  ismkv  7145  ismkvnex  7147  mkvprop  7150  fodjumkvlemres  7151  enmkvlem  7153  iswomni  7157  exmidfodomrlemr  7195  exmidfodomrlemrALT  7196  tapeq1  7242  ccfunen  7251  ltsonq  7385  ltexnqq  7395  prcdnql  7471  prcunqu  7472  prloc  7478  prdisj  7479  genprndl  7508  genprndu  7509  caucvgprlemnkj  7653  caucvgprlemnbj  7654  caucvgprlemcl  7663  caucvgprprlemcbv  7674  caucvgprprlemval  7675  suplocexprlemloc  7708  lttrsr  7749  ltsosr  7751  recexgt0sr  7760  mulgt0sr  7765  aptisr  7766  mulextsr1  7768  srpospr  7770  caucvgsrlemgt1  7782  caucvgsrlemoffres  7787  caucvgsr  7789  map2psrprg  7792  suplocsrlemb  7793  axprecex  7867  axpre-ltwlin  7870  axpre-lttrn  7871  axpre-apti  7872  axpre-mulgt0  7874  axpre-mulext  7875  axcaucvglemcau  7885  axcaucvglemres  7886  axpre-suploclemres  7888  axpre-suploc  7889  axsuploc  8017  ltleletr  8026  ltordlem  8426  squeeze0  8847  sup3exmid  8900  nnsub  8944  fzind  9354  uzind4s  9576  uzind4s2  9577  indstr  9579  supinfneg  9581  infsupneg  9582  frec2uzuzd  10385  frec2uzltd  10386  uzsinds  10425  seq3fveq2  10452  seq3shft2  10456  monoord  10459  seq3split  10462  seq3id2  10492  expcl2lemap  10515  nn0ltexp2  10671  facdiv  10699  facwordi  10701  zfz1isolem1  10801  zfz1iso  10802  seq3coll  10803  caucvgre  10971  fimaxre2  11216  climcn1  11297  climcn2  11298  subcn2  11300  summodclem2a  11370  fsumsplitf  11397  fsum2d  11424  modfsummod  11447  fsumabs  11454  telfsumo  11455  fsumiun  11466  prodfdivap  11536  fprod2d  11612  fproddivapf  11620  fprodsplitf  11621  fprodsplit1f  11623  ndvdssub  11915  bezoutlemmain  11979  bezoutlemex  11982  bezoutlemzz  11983  bezoutlemsup  11990  dfgcd2  11995  algcvg  12028  algcvga  12031  algfx  12032  lcmgcdlem  12057  lcmdvds  12059  coprmgcdb  12068  coprmdvds1  12071  coprmdvds2  12073  prmind2  12100  dvdsprime  12102  nprm  12103  dvdsprm  12117  exprmfct  12118  isprm5lem  12121  coprm  12124  isprm6  12127  prmfac1  12132  sqrt2irr  12142  pcqmul  12283  pcqcl  12286  pc2dvds  12309  pcz  12311  prmpwdvds  12333  ennnfonelemim  12405  exmidunben  12407  infpn2  12437  mhmlem  12864  uniopn  13163  fiinopn  13166  epttop  13254  cnpval  13362  iscnp  13363  icnpimaex  13375  lmcvg  13381  cnptoprest  13403  cnptoprest2  13404  lmss  13410  lmff  13413  txcnp  13435  txlm  13443  cnmpt12  13451  cnmpt22  13458  blssps  13591  blss  13592  metss  13658  comet  13663  metcnp3  13675  metcnp2  13677  txmetcnp  13682  divcnap  13719  elcncf2  13725  cncfi  13729  mulc1cncf  13740  cncfmet  13743  mulcncflem  13754  mulcncf  13755  dedekindeulemloc  13761  dedekindeulemlu  13763  dedekindeulemeu  13764  suplociccreex  13766  dedekindicclemloc  13770  dedekindicclemlu  13772  dedekindicclemeu  13773  ivthinclemlopn  13778  ivthinclemlr  13779  ivthinclemuopn  13780  ivthinclemur  13781  ivthinclemloc  13783  limccl  13792  ellimc3apf  13793  limccnpcntop  13808  limccnp2lem  13809  limccoap  13811  dvcoapbr  13835  lgsdir2lem4  14096  2sqlem6  14120  2sqlem8  14123  2sqlem10  14125  cbvrald  14193  bj-bdfindes  14354  bj-omtrans  14361  bj-inf2vnlem1  14375  bj-inf2vnlem2  14376  bj-inf2vnlem3  14377  bj-inf2vnlem4  14378  bj-findes  14386  strcoll2  14388  sscoll2  14393  subctctexmid  14403  pw1nct  14405  exmidsbthrlem  14423  sbthom  14427  apdiff  14449  ismkvnnlem  14453  nconstwlpolem  14465  neapmkv  14468
  Copyright terms: Public domain W3C validator