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  833  nfbidf  1550  drnf1  1744  drnf2  1745  equveli  1770  ax11v2  1831  ax11v  1838  ax11ev  1839  equs5or  1841  mobidh  2076  mobid  2077  axext3  2176  cbvralfw  2716  cbvralf  2718  cbvralvw  2730  cbvraldva2  2733  gencbval  2809  vtoclgaf  2826  vtocl2gaf  2828  vtocl3gaf  2830  rspct  2858  rspc  2859  rspc2gv  2877  ceqex  2888  ralab2  2925  mob2  2941  mob  2943  morex  2945  reu7  2956  reu8  2957  nelrdva  2968  cdeqim  2979  sbcimg  3028  csbhypf  3120  cbvralcsf  3144  dfss2f  3171  sbcssg  3556  sneqrg  3789  elintab  3882  intss1  3886  intmin  3891  dfiin2g  3946  disji2  4023  disjiun  4025  trel  4135  trss  4137  bnd2  4203  zfpow  4205  exmidexmid  4226  exmidsssnc  4233  exmidundifim  4237  exmid1stab  4238  rext  4245  opth  4267  copsexg  4274  poeq1  4331  pocl  4335  swopolem  4337  swopo  4338  soeq1  4347  sowlin  4352  frforeq2  4377  frforeq3  4379  frirrg  4382  frind  4384  weeq1  4388  ordelord  4413  reusv3i  4491  ordtriexmid  4554  ontr2exmid  4558  onsucsssucexmid  4560  onsucelsucexmid  4563  ordsucunielexmid  4564  regexmidlem1  4566  regexmid  4568  reg2exmid  4569  elirr  4574  en2lp  4587  ordsoexmid  4595  onintexmid  4606  reg3exmid  4613  tfis  4616  tfisi  4620  peano2  4628  findes  4636  nnregexmid  4654  omsinds  4655  vtoclr  4708  poinxp  4729  soinxp  4730  posng  4732  ssrel  4748  ssrel2  4750  ssrelrel  4760  relop  4813  issref  5049  iotaexab  5234  iota5  5237  dffun4f  5271  sbcfung  5279  funopg  5289  brprcneu  5548  funfveu  5568  tz6.12f  5584  funbrfv  5596  ssimaexg  5620  fvmptss2  5633  fvmptssdm  5643  fvmptf  5651  fvelrn  5690  f1veqaeq  5813  dff13f  5814  isopolem  5866  isosolem  5868  riota5f  5899  imbrov2fvoveq  5944  oprabid  5951  ovmpos  6043  ov2gf  6044  ovi3  6057  caovcan  6085  caovordig  6086  caofrss  6159  caoftrn  6160  dfoprab4f  6248  f1o2ndf1  6283  poxp  6287  smoel  6355  tfrlem1  6363  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemaccex  6403  tfr1onlemres  6404  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemaccex  6416  tfrcllemres  6417  tfrcl  6419  nnsucelsuc  6546  nnsucsssuc  6547  nnmordi  6571  nnaordex  6583  qsel  6668  eroveu  6682  ecopovtrn  6688  ecopovtrng  6691  th3qlem2  6694  ixpsnf1o  6792  fundmeng  6863  phplem3g  6914  nneneq  6915  ssfiexmid  6934  domfiexmid  6936  findcard  6946  findcard2  6947  findcard2s  6948  findcard2d  6949  findcard2sd  6950  diffifi  6952  ac6sfi  6956  fiintim  6987  fisseneq  6990  fidcenumlemrk  7015  fidcenumlemr  7016  isbth  7028  supeq3  7051  supeq123d  7052  supmoti  7054  suplubti  7061  supisolem  7069  cnvinfex  7079  eqinfti  7081  infvalti  7083  ordiso2  7096  nninfninc  7184  nnnninfeq2  7190  isomni  7197  finomni  7201  exmidomni  7203  ctssexmid  7211  ismkv  7214  ismkvnex  7216  mkvprop  7219  fodjumkvlemres  7220  enmkvlem  7222  iswomni  7226  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  tapeq1  7314  exmidapne  7322  ccfunen  7326  ltsonq  7460  ltexnqq  7470  prcdnql  7546  prcunqu  7547  prloc  7553  prdisj  7554  genprndl  7583  genprndu  7584  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemcl  7738  caucvgprprlemcbv  7749  caucvgprprlemval  7750  suplocexprlemloc  7783  lttrsr  7824  ltsosr  7826  recexgt0sr  7835  mulgt0sr  7840  aptisr  7841  mulextsr1  7843  srpospr  7845  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  caucvgsr  7864  map2psrprg  7867  suplocsrlemb  7868  axprecex  7942  axpre-ltwlin  7945  axpre-lttrn  7946  axpre-apti  7947  axpre-mulgt0  7949  axpre-mulext  7950  axcaucvglemcau  7960  axcaucvglemres  7961  axpre-suploclemres  7963  axpre-suploc  7964  axsuploc  8094  ltleletr  8103  ltordlem  8503  squeeze0  8925  sup3exmid  8978  nnsub  9023  fzind  9435  uzind4s  9658  uzind4s2  9659  indstr  9661  supinfneg  9663  infsupneg  9664  frec2uzuzd  10476  frec2uzltd  10477  uzsinds  10518  seq3fveq2  10549  seqfveq2g  10551  seq3shft2  10555  seqshft2g  10556  monoord  10559  seq3split  10562  seqsplitg  10563  seqf1oglem2  10594  seqf1og  10595  seq3id2  10600  seqhomog  10604  expcl2lemap  10625  nn0ltexp2  10783  facdiv  10812  facwordi  10814  zfz1isolem1  10914  zfz1iso  10915  seq3coll  10916  caucvgre  11128  fimaxre2  11373  climcn1  11454  climcn2  11455  subcn2  11457  summodclem2a  11527  fsumsplitf  11554  fsum2d  11581  modfsummod  11604  fsumabs  11611  telfsumo  11612  fsumiun  11623  prodfdivap  11693  fprod2d  11769  fproddivapf  11777  fprodsplitf  11778  fprodsplit1f  11780  ndvdssub  12074  bezoutlemmain  12138  bezoutlemex  12141  bezoutlemzz  12142  bezoutlemsup  12149  dfgcd2  12154  algcvg  12189  algcvga  12192  algfx  12193  lcmgcdlem  12218  lcmdvds  12220  coprmgcdb  12229  coprmdvds1  12232  coprmdvds2  12234  prmind2  12261  dvdsprime  12263  nprm  12264  dvdsprm  12278  exprmfct  12279  isprm5lem  12282  coprm  12285  isprm6  12288  prmfac1  12293  sqrt2irr  12303  pcqmul  12444  pcqcl  12447  pc2dvds  12471  pcz  12473  prmpwdvds  12496  ennnfonelemim  12584  exmidunben  12586  infpn2  12616  setscomd  12662  mhmlem  13187  isnsg2  13276  ghmf1  13346  islring  13691  lringuplu  13695  rrgval  13761  rrgeq0i  13763  isdomn  13768  domneq0  13771  opprdomnbg  13773  znidom  14156  znrrg  14159  uniopn  14180  fiinopn  14183  epttop  14269  cnpval  14377  iscnp  14378  icnpimaex  14390  lmcvg  14396  cnptoprest  14418  cnptoprest2  14419  lmss  14425  lmff  14428  txcnp  14450  txlm  14458  cnmpt12  14466  cnmpt22  14473  blssps  14606  blss  14607  metss  14673  comet  14678  metcnp3  14690  metcnp2  14692  txmetcnp  14697  divcnap  14744  mpomulcn  14745  elcncf2  14753  cncfi  14757  mulc1cncf  14768  cncfmet  14771  mulcncflem  14786  mulcncf  14787  dedekindeulemloc  14798  dedekindeulemlu  14800  dedekindeulemeu  14801  suplociccreex  14803  dedekindicclemloc  14807  dedekindicclemlu  14809  dedekindicclemeu  14810  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemloc  14820  ivthreinc  14824  limccl  14838  ellimc3apf  14839  limccnpcntop  14854  limccnp2lem  14855  limccoap  14857  dvcoapbr  14886  dvmptfsum  14904  lgsdir2lem4  15188  gausslemma2dlem0i  15214  lgseisenlem2  15228  lgsquad2lem2  15239  2sqlem6  15277  2sqlem8  15280  2sqlem10  15282  cbvrald  15350  bj-bdfindes  15511  bj-omtrans  15518  bj-inf2vnlem1  15532  bj-inf2vnlem2  15533  bj-inf2vnlem3  15534  bj-inf2vnlem4  15535  bj-findes  15543  strcoll2  15545  sscoll2  15550  subctctexmid  15561  pw1nct  15563  exmidsbthrlem  15582  sbthom  15586  apdiff  15608  ismkvnnlem  15612  nconstwlpolem  15625  neapmkv  15628  neap0mkv  15629  ltlenmkv  15630
  Copyright terms: Public domain W3C validator