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

Theorem anbi2d 452
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 438 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  anbi2  455  anbi12d  457  bi2anan9  571  dn1dc  904  xorbi2d  1314  dfbi3dc  1331  xordidc  1333  eleq2w  2146  eleq2  2148  ceqsex2  2653  ceqsex6v  2657  vtocl2gaf  2679  ceqsrex2v  2740  mob2  2786  eqreu  2798  nelrdva  2811  dfss4st  3221  undif4  3333  r19.27m  3364  ifbi  3397  preq12bg  3600  opeq2  3606  ralunsn  3624  intab  3700  opabbid  3878  opthg  4039  pocl  4104  ordelord  4182  ordtriexmid  4311  ontr2exmid  4314  onsucsssucexmid  4316  tfisi  4375  xpeq2  4426  rabxp  4446  vtoclr  4454  opeliunxp  4461  posng  4478  opbrop  4485  rexiunxp  4546  elrnmpt1  4654  dfres2  4731  brcodir  4786  poltletr  4799  xp11m  4835  elxp4  4884  elxp5  4885  dffun4f  4997  fununi  5047  fneq2  5068  fnun  5085  feq3  5112  foeq3  5194  funfveu  5281  funbrfv  5306  ssimaexg  5329  fvopab3g  5340  fvopab3ig  5341  fvelrn  5393  fmptco  5427  fsn2  5434  elunirn  5506  isoeq2  5542  isoeq3  5543  isocnv2  5552  isoini  5558  isopolem  5562  f1oiso  5566  f1oiso2  5567  oprabbid  5659  cbvoprab3  5681  mpt2mptx  5696  mpt2fun  5704  ov  5721  ovi3  5738  ov6g  5739  ovg  5740  caoftrn  5837  f1o2ndf1  5950  xporderlem  5953  f1od2  5957  brtpos2  5970  brtposg  5973  dftpos4  5982  recseq  6025  tfrlem3-2d  6031  tfrlemi1  6051  tfrexlem  6053  tfr1onlemaccex  6067  tfrcllemaccex  6080  tfrcl  6083  freceq1  6111  freceq2  6112  frecsuc  6126  nnaordex  6238  brecop  6334  eroveu  6335  erovlem  6336  ecopovtrn  6341  ecopovtrng  6344  th3qlem1  6346  th3qlem2  6347  th3q  6349  elpmg  6373  domeng  6421  dom2lem  6441  xpcomco  6494  xpassen  6498  xpdom2  6499  xpf1o  6512  phplem3g  6524  ssfiexmid  6544  domfiexmid  6546  findcard2  6557  findcard2s  6558  findcard2d  6559  findcard2sd  6560  diffifi  6562  supeq2  6628  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  recexnq  6893  recmulnqg  6894  ltsonq  6901  enq0sym  6935  enq0ref  6936  enq0tr  6937  enq0breq  6939  addnq0mo  6950  mulnq0mo  6951  addnnnq0  6952  mulnnnq0  6953  elinp  6977  prdisj  6995  prarloclem3  7000  prarloc  7006  distrlem5prl  7089  distrlem5pru  7090  ltexprlemell  7101  ltexprlemelu  7102  recexprlemm  7127  addsrmo  7233  mulsrmo  7234  addsrpr  7235  mulsrpr  7236  lttrsr  7252  recexgt0sr  7263  mulgt0sr  7267  ltresr  7320  axprecex  7359  axpre-lttrn  7363  axpre-mulgt0  7366  lesub0  7901  apreap  8005  apreim  8021  zltlen  8758  prime  8778  fzind  8794  qltlen  9057  xltnegi  9229  ixxval  9246  fzval  9358  fzdifsuc  9425  elfzm11  9435  elfzo  9488  exbtwnzlemshrink  9588  rebtwn2zlemshrink  9593  facwordi  10044  zfz1iso  10142  shftfvalg  10148  shftfibg  10150  shftfval  10151  shftfib  10153  shftfn  10154  2shfti  10161  cau3lem  10442  caubnd2  10445  clim  10562  clim2  10564  climi  10568  climcn2  10590  addcn2  10591  subcn2  10592  mulcn2  10593  isummolem2a  10660  isummo  10662  fisum  10665  divalgb  10800  ndvdssub  10805  zsupcllemex  10817  gcdval  10826  gcdneg  10848  bezoutlemstep  10861  bezoutlemmain  10862  bezoutlemex  10865  dfgcd2  10878  gcdass  10879  algcvgblem  10906  lcmval  10920  lcmneg  10931  lcmgcdlem  10934  lcmass  10942  qredeq  10953  prmind2  10977  euclemma  11000  pw2dvdslemn  11018  qnumval  11038  qdenval  11039
  Copyright terms: Public domain W3C validator