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

Theorem imbi12d 223
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 220 . 2 (φ → ((ψθ) ↔ (χθ)))
3 imbi12d.2 . . 3 (φ → (θτ))
43imbi2d 219 . 2 (φ → ((χθ) ↔ (χτ)))
52, 4bitrd 177 1 (φ → ((ψθ) ↔ (χτ)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  nfbidf  1406  drnf1  1595  drnf2  1596  equveli  1616  ax11v2  1675  ax11v  1682  ax11ev  1683  equs5or  1685  mobidh  1908  mobid  1909  axext3  1997  cbvralf  2497  cbvraldva2  2507  gencbval  2571  vtoclgaf  2587  vtocl2gaf  2589  vtocl3gaf  2591  rspct  2618  rspc  2619  ceqex  2640  ralab2  2674  mob2  2690  mob  2692  morex  2694  reu7  2705  reu8  2706  nelrdva  2715  cdeqim  2726  sbcimg  2773  csbhypf  2854  cbvralcsf  2877  dfss2f  2905  sbcssg  3299  sneqrg  3497  elintab  3590  intss1  3594  intmin  3599  dfiin2g  3654  trel  3825  trss  3827  bnd2  3890  zfpow  3892  rext  3915  opth  3938  copsexg  3945  poeq1  4000  pocl  4004  swopolem  4006  swopo  4007  soeq1  4016  sowlin  4021  ordelord  4057  reusv3i  4130  ordtriexmid  4183  onsucsssucexmid  4185  onsucelsucexmid  4188  ordsucunielexmid  4189  regexmidlem1  4191  regexmid  4192  elirr  4197  en2lp  4205  ordsoexmid  4213  tfis  4222  tfisi  4226  peano2  4234  findes  4242  nnregexmid  4258  vtoclr  4304  poinxp  4325  soinxp  4326  posng  4328  ssrel  4344  ssrel2  4346  ssrelrel  4356  relop  4402  issref  4623  iota5  4803  dffun4f  4833  sbcfung  4840  funopg  4849  brprcneu  5085  funfveu  5102  tz6.12f  5116  funbrfv  5126  ssimaexg  5149  fvmptss2  5161  fvmptssdm  5169  fvmptf  5177  fvelrn  5212  f1veqaeq  5322  dff13f  5323  isopolem  5375  isosolem  5377  riota5f  5405  oprabid  5450  ovmpt2s  5536  ov2gf  5537  ovi3  5549  caovcan  5577  caovordig  5578  caofrss  5647  caoftrn  5648  dfoprab4f  5731  f1o2ndf1  5761  poxp  5764  smoel  5826  tfrlem1  5834  nnsucelsuc  5974  nnsucsssuc  5975  nnmordi  5989  nnaordex  6000  qsel  6083  eroveu  6097  ecopovtrn  6103  ecopovtrng  6106  th3qlem2  6109  ltsonq  6244  ltexnqq  6253  prcdnql  6325  prcunqu  6326  prloc  6332  prdisj  6333  genprndl  6363  genprndu  6364  lttrsr  6501  ltsosr  6503  recexgt0sr  6512  mulgt0sr  6515  aptisr  6516  mulextsr1  6518  axprecex  6570  axpre-ltwlin  6573  axpre-lttrn  6574  axpre-apti  6575  axpre-mulgt0  6577  axpre-mulext  6578  ltleletr  6701  squeeze0  7454  nnsub  7536  fzind  7919  cbvrald  8264  bj-bdfindes  8405  bj-omtrans  8412  bj-inf2vnlem1  8422  bj-inf2vnlem2  8423  bj-inf2vnlem3  8424  bj-inf2vnlem4  8425  bj-findes  8433  strcoll2  8435  sscoll2  8440
  Copyright terms: Public domain W3C validator