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  580  dn1dc  929  xorbi2d  1343  dfbi3dc  1360  xordidc  1362  eleq2w  2179  eleq2  2181  ceqsex2  2700  ceqsex6v  2704  vtocl2gaf  2727  ceqsrex2v  2791  mob2  2837  eqreu  2849  nelrdva  2864  dfss4st  3279  undif4  3395  r19.27m  3428  ifbi  3462  preq12bg  3670  opeq2  3676  ralunsn  3694  intab  3770  disjiun  3894  brimralrspcev  3957  opabbid  3963  opthg  4130  pocl  4195  ordelord  4273  ordtriexmid  4407  ontr2exmid  4410  onsucsssucexmid  4412  tfisi  4471  xpeq2  4524  rabxp  4546  vtoclr  4557  opeliunxp  4564  posng  4581  opbrop  4588  rexiunxp  4651  elrnmpt1  4760  dfres2  4841  brcodir  4896  poltletr  4909  xp11m  4947  elxp4  4996  elxp5  4997  dffun4f  5109  fununi  5161  fneq2  5182  fnun  5199  feq3  5227  foeq3  5313  funfveu  5402  funbrfv  5428  ssimaexg  5451  fvopab3g  5462  fvopab3ig  5463  fvelrn  5519  fmptco  5554  fsn2  5562  elunirn  5635  isoeq2  5671  isoeq3  5672  isocnv2  5681  isoini  5687  isopolem  5691  f1oiso  5695  f1oiso2  5696  oprabbid  5792  cbvoprab3  5815  mpomptx  5830  mpofun  5841  ov  5858  ovi3  5875  ov6g  5876  ovg  5877  caoftrn  5975  f1o2ndf1  6093  xporderlem  6096  f1od2  6100  brtpos2  6116  brtposg  6119  dftpos4  6128  recseq  6171  tfrlem3-2d  6177  tfrlemi1  6197  tfrexlem  6199  tfr1onlemaccex  6213  tfrcllemaccex  6226  tfrcl  6229  freceq1  6257  freceq2  6258  frecsuc  6272  nnaordex  6391  brecop  6487  eroveu  6488  erovlem  6489  ecopovtrn  6494  ecopovtrng  6497  th3qlem1  6499  th3qlem2  6500  th3q  6502  elpmg  6526  ixpsnval  6563  ixpsnf1o  6598  domeng  6614  dom2lem  6634  xpcomco  6688  xpassen  6692  xpdom2  6693  xpf1o  6706  phplem3g  6718  ssfiexmid  6738  domfiexmid  6740  findcard2  6751  findcard2s  6752  findcard2d  6753  findcard2sd  6754  diffifi  6756  fiintim  6785  fidcenumlemrk  6810  fidcenumlemr  6811  supeq2  6844  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  acfun  7031  ccfunen  7047  recexnq  7166  recmulnqg  7167  ltsonq  7174  enq0sym  7208  enq0ref  7209  enq0tr  7210  enq0breq  7212  addnq0mo  7223  mulnq0mo  7224  addnnnq0  7225  mulnnnq0  7226  elinp  7250  prdisj  7268  prarloclem3  7273  prarloc  7279  distrlem5prl  7362  distrlem5pru  7363  ltexprlemell  7374  ltexprlemelu  7375  recexprlemm  7400  addsrmo  7519  mulsrmo  7520  addsrpr  7521  mulsrpr  7522  lttrsr  7538  recexgt0sr  7549  mulgt0sr  7554  ltresr  7615  axprecex  7656  axpre-lttrn  7660  axpre-mulgt0  7663  lesub0  8209  apreap  8316  apreim  8332  aprcl  8375  zltlen  9087  prime  9108  fzind  9124  qltlen  9388  xltnegi  9573  ixxval  9634  fzval  9747  fzdifsuc  9816  elfzm11  9826  elfzo  9881  exbtwnzlemshrink  9981  rebtwn2zlemshrink  9986  facwordi  10441  zfz1iso  10539  shftfvalg  10545  shftfibg  10547  shftfval  10548  shftfib  10550  shftfn  10551  2shfti  10558  cau3lem  10841  caubnd2  10844  xrmaxiflemcom  10973  clim  11005  clim2  11007  climi  11011  climcn2  11033  addcn2  11034  subcn2  11035  mulcn2  11036  summodclem2a  11105  summodc  11107  fsum3  11111  fsumsplitf  11132  sinbnd  11373  cosbnd  11374  divalgb  11534  ndvdssub  11539  zsupcllemex  11551  gcdval  11560  gcdneg  11582  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlemex  11601  dfgcd2  11614  gcdass  11615  algcvgblem  11642  lcmval  11656  lcmneg  11667  lcmgcdlem  11670  lcmass  11678  qredeq  11689  prmind2  11713  euclemma  11736  pw2dvdslemn  11754  qnumval  11774  qdenval  11775  basis2  12126  eltg2  12133  isnei  12224  isneip  12226  restbasg  12248  iscnp  12279  iscnp3  12283  tgcn  12288  icnpimaex  12291  lmbrf  12295  cncnp  12310  cnptoprest2  12320  txbas  12338  txcnp  12351  imasnopn  12379  ispsmet  12403  ismet  12424  isxmet  12425  ismet2  12434  blres  12514  metcnp3  12591  txmetcnp  12598  mulcncf  12671  ellimc3apf  12709  limcdifap  12711  limcmpted  12712  limccnp2lem  12725  sincosq3sgn  12820  subctctexmid  13092
  Copyright terms: Public domain W3C validator