ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi2d 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  867  xorbi2d  1271  dfbi3dc  1288  xordidc  1290  eleq2  2101  ceqsex2  2594  ceqsex6v  2598  vtocl2gaf  2620  ceqsrex2v  2676  mob2  2721  eqreu  2733  nelrdva  2746  psssstr  3051  undif4  3284  r19.27m  3316  ifbi  3348  preq12bg  3544  opeq2  3550  ralunsn  3568  intab  3644  opabbid  3822  opthg  3975  pocl  4040  ordelord  4118  ordtriexmid  4247  ontr2exmid  4250  onsucsssucexmid  4252  tfisi  4310  xpeq2  4360  rabxp  4380  vtoclr  4388  opeliunxp  4395  posng  4412  opbrop  4419  rexiunxp  4478  elrnmpt1  4585  dfres2  4658  brcodir  4712  poltletr  4725  xp11m  4759  elxp4  4808  elxp5  4809  dffun4f  4918  fununi  4967  fneq2  4988  fnun  5005  feq3  5032  foeq3  5104  funfveu  5188  funbrfv  5212  ssimaexg  5235  fvopab3g  5245  fvopab3ig  5246  fvelrn  5298  fmptco  5330  fsn2  5337  elunirn  5405  isoeq2  5442  isoeq3  5443  isocnv2  5452  isoini  5457  isopolem  5461  f1oiso  5465  f1oiso2  5466  oprabbid  5558  cbvoprab3  5580  mpt2mptx  5595  mpt2fun  5603  ov  5620  ovi3  5637  ov6g  5638  ovg  5639  caoftrn  5736  f1o2ndf1  5849  xporderlem  5852  brtpos2  5866  brtposg  5869  dftpos4  5878  recseq  5921  tfrlem3-2  5927  tfrlem3-2d  5928  tfrlemi1  5946  tfrexlem  5948  freceq1  5979  freceq2  5980  frecsuc  5991  nnaordex  6100  brecop  6196  eroveu  6197  erovlem  6198  ecopovtrn  6203  ecopovtrng  6206  th3qlem1  6208  th3qlem2  6209  th3q  6211  domeng  6233  dom2lem  6252  xpcomco  6300  xpassen  6304  xpdom2  6305  phplem3g  6319  ssfiexmid  6336  findcard2  6346  findcard2s  6347  findcard2d  6348  findcard2sd  6349  diffifi  6351  recexnq  6486  recmulnqg  6487  ltsonq  6494  enq0sym  6528  enq0ref  6529  enq0tr  6530  enq0breq  6532  addnq0mo  6543  mulnq0mo  6544  addnnnq0  6545  mulnnnq0  6546  elinp  6570  prdisj  6588  prarloclem3  6593  prarloc  6599  distrlem5prl  6682  distrlem5pru  6683  ltexprlemell  6694  ltexprlemelu  6695  recexprlemm  6720  addsrmo  6826  mulsrmo  6827  addsrpr  6828  mulsrpr  6829  lttrsr  6845  recexgt0sr  6856  mulgt0sr  6860  ltresr  6913  axprecex  6952  axpre-lttrn  6956  axpre-mulgt0  6959  lesub0  7472  apreap  7576  apreim  7592  zltlen  8317  prime  8335  fzind  8351  qltlen  8573  xltnegi  8746  ixxval  8763  fzval  8874  fzdifsuc  8941  elfzm11  8951  elfzo  9004  qbtwnzlemshrink  9102  rebtwn2zlemshrink  9106  shftfvalg  9417  shftfibg  9419  shftfval  9420  shftfib  9422  shftfn  9423  2shfti  9430  cau3lem  9708  caubnd2  9711  clim  9800  clim2  9802  climi  9806  climcn2  9828  addcn2  9829  subcn2  9830  mulcn2  9831  algcvgblem  9886
  Copyright terms: Public domain W3C validator