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

Theorem anbi2d 459
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 445 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  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:  anbi2  462  anbi12d  464  bi2anan9  595  dn1dc  944  xorbi2d  1358  dfbi3dc  1375  xordidc  1377  eleq2w  2201  eleq2  2203  ceqsex2  2726  ceqsex6v  2730  vtocl2gaf  2753  ceqsrex2v  2817  mob2  2864  eqreu  2876  nelrdva  2891  dfss4st  3309  undif4  3425  r19.27m  3458  ifbi  3492  preq12bg  3700  opeq2  3706  ralunsn  3724  intab  3800  disjiun  3924  brimralrspcev  3987  opabbid  3993  opthg  4160  pocl  4225  ordelord  4303  ordtriexmid  4437  ontr2exmid  4440  onsucsssucexmid  4442  tfisi  4501  xpeq2  4554  rabxp  4576  vtoclr  4587  opeliunxp  4594  posng  4611  opbrop  4618  rexiunxp  4681  elrnmpt1  4790  dfres2  4871  brcodir  4926  poltletr  4939  xp11m  4977  elxp4  5026  elxp5  5027  dffun4f  5139  fununi  5191  fneq2  5212  fnun  5229  feq3  5257  foeq3  5343  funfveu  5434  funbrfv  5460  ssimaexg  5483  fvopab3g  5494  fvopab3ig  5495  fvelrn  5551  fmptco  5586  fsn2  5594  elunirn  5667  isoeq2  5703  isoeq3  5704  isocnv2  5713  isoini  5719  isopolem  5723  f1oiso  5727  f1oiso2  5728  oprabbid  5824  cbvoprab3  5847  mpomptx  5862  mpofun  5873  ov  5890  ovi3  5907  ov6g  5908  ovg  5909  caoftrn  6007  f1o2ndf1  6125  xporderlem  6128  f1od2  6132  brtpos2  6148  brtposg  6151  dftpos4  6160  recseq  6203  tfrlem3-2d  6209  tfrlemi1  6229  tfrexlem  6231  tfr1onlemaccex  6245  tfrcllemaccex  6258  tfrcl  6261  freceq1  6289  freceq2  6290  frecsuc  6304  nnaordex  6423  brecop  6519  eroveu  6520  erovlem  6521  ecopovtrn  6526  ecopovtrng  6529  th3qlem1  6531  th3qlem2  6532  th3q  6534  elpmg  6558  ixpsnval  6595  ixpsnf1o  6630  domeng  6646  dom2lem  6666  xpcomco  6720  xpassen  6724  xpdom2  6725  xpf1o  6738  phplem3g  6750  ssfiexmid  6770  domfiexmid  6772  findcard2  6783  findcard2s  6784  findcard2d  6785  findcard2sd  6786  diffifi  6788  fiintim  6817  fidcenumlemrk  6842  fidcenumlemr  6843  supeq2  6876  exmidfodomrlemr  7063  exmidfodomrlemrALT  7064  acfun  7068  ccfunen  7084  recexnq  7210  recmulnqg  7211  ltsonq  7218  enq0sym  7252  enq0ref  7253  enq0tr  7254  enq0breq  7256  addnq0mo  7267  mulnq0mo  7268  addnnnq0  7269  mulnnnq0  7270  elinp  7294  prdisj  7312  prarloclem3  7317  prarloc  7323  distrlem5prl  7406  distrlem5pru  7407  ltexprlemell  7418  ltexprlemelu  7419  recexprlemm  7444  addsrmo  7563  mulsrmo  7564  addsrpr  7565  mulsrpr  7566  lttrsr  7582  recexgt0sr  7593  mulgt0sr  7598  ltresr  7659  axprecex  7700  axpre-lttrn  7704  axpre-mulgt0  7707  lesub0  8253  apreap  8361  apreim  8377  aprcl  8420  zltlen  9141  prime  9162  fzind  9178  qltlen  9444  xltnegi  9630  ixxval  9691  fzval  9804  fzdifsuc  9873  elfzm11  9883  elfzo  9938  exbtwnzlemshrink  10038  rebtwn2zlemshrink  10043  facwordi  10498  zfz1iso  10596  shftfvalg  10602  shftfibg  10604  shftfval  10605  shftfib  10607  shftfn  10608  2shfti  10615  cau3lem  10898  caubnd2  10901  xrmaxiflemcom  11030  clim  11062  clim2  11064  climi  11068  climcn2  11090  addcn2  11091  subcn2  11092  mulcn2  11093  summodclem2a  11162  summodc  11164  fsum3  11168  fsumsplitf  11189  prodfdivap  11328  ntrivcvgap0  11330  prodeq1f  11333  prodeq2w  11337  prodeq2  11338  prodmodc  11359  sinbnd  11470  cosbnd  11471  divalgb  11633  ndvdssub  11638  zsupcllemex  11650  gcdval  11659  gcdneg  11681  bezoutlemstep  11696  bezoutlemmain  11697  bezoutlemex  11700  dfgcd2  11713  gcdass  11714  algcvgblem  11741  lcmval  11755  lcmneg  11766  lcmgcdlem  11769  lcmass  11777  qredeq  11788  prmind2  11812  euclemma  11835  pw2dvdslemn  11854  qnumval  11874  qdenval  11875  basis2  12229  eltg2  12236  isnei  12327  isneip  12329  restbasg  12351  iscnp  12382  iscnp3  12386  tgcn  12391  icnpimaex  12394  lmbrf  12398  cncnp  12413  cnptoprest2  12423  txbas  12441  txcnp  12454  imasnopn  12482  ispsmet  12506  ismet  12527  isxmet  12528  ismet2  12537  blres  12617  metcnp3  12694  txmetcnp  12701  mulcncf  12774  ellimc3apf  12812  limcdifap  12814  limcmpted  12815  limccnp2lem  12828  sincosq3sgn  12931  subctctexmid  13255
  Copyright terms: Public domain W3C validator