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  8630  sup3exmid  8683  nnsub  8727  fzind  9134  uzind4s  9353  uzind4s2  9354  indstr  9356  supinfneg  9358  infsupneg  9359  frec2uzuzd  10143  frec2uzltd  10144  uzsinds  10183  seq3fveq2  10210  seq3shft2  10214  monoord  10217  seq3split  10220  seq3id2  10250  expcl2lemap  10273  facdiv  10452  facwordi  10454  zfz1isolem1  10551  zfz1iso  10552  seq3coll  10553  caucvgre  10721  fimaxre2  10966  climcn1  11045  climcn2  11046  subcn2  11048  summodclem2a  11118  fsumsplitf  11145  fsum2d  11172  modfsummod  11195  fsumabs  11202  telfsumo  11203  fsumiun  11214  ndvdssub  11554  bezoutlemmain  11613  bezoutlemex  11616  bezoutlemzz  11617  bezoutlemsup  11624  dfgcd2  11629  algcvg  11656  algcvga  11659  algfx  11660  lcmgcdlem  11685  lcmdvds  11687  coprmgcdb  11696  coprmdvds1  11699  coprmdvds2  11701  prmind2  11728  dvdsprime  11730  nprm  11731  dvdsprm  11744  exprmfct  11745  coprm  11749  isprm6  11752  prmfac1  11757  sqrt2irr  11767  ennnfonelemim  11864  exmidunben  11866  uniopn  12095  fiinopn  12098  epttop  12186  cnpval  12294  iscnp  12295  icnpimaex  12307  lmcvg  12313  cnptoprest  12335  cnptoprest2  12336  lmss  12342  lmff  12345  txcnp  12367  txlm  12375  cnmpt12  12383  cnmpt22  12390  blssps  12523  blss  12524  metss  12590  comet  12595  metcnp3  12607  metcnp2  12609  txmetcnp  12614  divcnap  12651  elcncf2  12657  cncfi  12661  mulc1cncf  12672  cncfmet  12675  mulcncflem  12686  mulcncf  12687  dedekindeulemloc  12693  dedekindeulemlu  12695  dedekindeulemeu  12696  suplociccreex  12698  dedekindicclemloc  12702  dedekindicclemlu  12704  dedekindicclemeu  12705  ivthinclemlopn  12710  ivthinclemlr  12711  ivthinclemuopn  12712  ivthinclemur  12713  ivthinclemloc  12715  limccl  12724  ellimc3apf  12725  limccnpcntop  12740  limccnp2lem  12741  limccoap  12743  dvcoapbr  12767  cbvrald  12922  bj-bdfindes  13074  bj-omtrans  13081  bj-inf2vnlem1  13095  bj-inf2vnlem2  13096  bj-inf2vnlem3  13097  bj-inf2vnlem4  13098  bj-findes  13106  strcoll2  13108  sscoll2  13113  exmid1stab  13122  subctctexmid  13123  exmidsbthrlem  13144  sbthom  13148
  Copyright terms: Public domain W3C validator