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

Theorem anbi2d 437
Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
anbid.1 (φ → (ψχ))
Assertion
Ref Expression
anbi2d (φ → ((θ ψ) ↔ (θ χ)))

Proof of Theorem anbi2d
StepHypRef Expression
1 anbid.1 . . 3 (φ → (ψχ))
21a1d 22 . 2 (φ → (θ → (ψχ)))
32pm5.32d 423 1 (φ → ((θ ψ) ↔ (θ χ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  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:  anbi2  440  anbi12d  442  bi2anan9  538  dn1dc  866  xorbi2d  1269  dfbi3dc  1285  xordidc  1287  eleq2  2098  ceqsex2  2588  ceqsex6v  2592  vtocl2gaf  2614  ceqsrex2v  2670  mob2  2715  eqreu  2727  nelrdva  2740  psssstr  3045  undif4  3278  r19.27m  3310  ifbi  3342  preq12bg  3535  opeq2  3541  ralunsn  3559  intab  3635  opabbid  3813  opthg  3966  pocl  4031  ordelord  4084  ordtriexmid  4210  onsucsssucexmid  4212  tfisi  4253  xpeq2  4303  rabxp  4323  vtoclr  4331  opeliunxp  4338  posng  4355  opbrop  4362  rexiunxp  4421  elrnmpt1  4528  dfres2  4601  brcodir  4655  poltletr  4668  xp11m  4702  elxp4  4751  elxp5  4752  dffun4f  4861  fununi  4910  fneq2  4931  fnun  4948  feq3  4975  foeq3  5047  funfveu  5131  funbrfv  5155  ssimaexg  5178  fvopab3g  5188  fvopab3ig  5189  fvelrn  5241  fmptco  5273  fsn2  5280  elunirn  5348  isoeq2  5385  isoeq3  5386  isocnv2  5395  isoini  5400  isopolem  5404  f1oiso  5408  f1oiso2  5409  oprabbid  5500  cbvoprab3  5522  mpt2mptx  5537  mpt2fun  5545  ov  5562  ovi3  5579  ov6g  5580  ovg  5581  caoftrn  5678  f1o2ndf1  5791  xporderlem  5793  brtpos2  5807  brtposg  5810  dftpos4  5819  recseq  5862  tfrlem3-2  5868  tfrlem3-2d  5869  tfrlemi1  5887  tfrexlem  5889  freceq1  5919  freceq2  5920  frecsuc  5930  nnaordex  6036  brecop  6132  eroveu  6133  erovlem  6134  ecopovtrn  6139  ecopovtrng  6142  th3qlem1  6144  th3qlem2  6145  th3q  6147  domeng  6169  dom2lem  6188  xpcomco  6236  xpassen  6240  xpdom2  6241  ssfiexmid  6254  recexnq  6374  recmulnqg  6375  ltsonq  6382  enq0sym  6414  enq0ref  6415  enq0tr  6416  enq0breq  6418  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  mulnnnq0  6432  elinp  6456  prdisj  6474  prarloclem3  6479  prarloc  6485  distrlem5prl  6561  distrlem5pru  6562  ltexprlemell  6571  ltexprlemelu  6572  recexprlemm  6595  addsrmo  6651  mulsrmo  6652  addsrpr  6653  mulsrpr  6654  lttrsr  6670  recexgt0sr  6681  mulgt0sr  6684  ltresr  6716  axprecex  6744  axpre-lttrn  6748  axpre-mulgt0  6751  lesub0  7249  apreap  7351  apreim  7367  zltlen  8075  prime  8093  fzind  8109  xltnegi  8498  ixxval  8515  fzval  8626  fzdifsuc  8693  elfzm11  8703  elfzo  8756
  Copyright terms: Public domain W3C validator