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

Theorem anbi1d 438
Description: Deduction adding a right 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
anbi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem anbi1d
StepHypRef Expression
1 anbid.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 22 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
32pm5.32rd 424 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:  anbi1  439  anbi12d  442  bi2anan9  538  pm5.71dc  868  xorbi1d  1272  drsb1  1680  ax11ev  1709  eleq1  2100  rexeqf  2499  reueq1f  2500  rmoeq1f  2501  rabeqf  2547  vtocl2gaf  2617  alexeq  2667  ceqex  2668  elrabi  2692  sbc5  2784  rexss  3004  psstr  3046  sspsstr  3047  ineq1  3128  difin2  3196  r19.28m  3308  preq12bg  3541  opeq1  3546  eluni  3580  mpteq12f  3834  axsep2  3873  zfauscl  3874  opthg  3972  copsexg  3978  euotd  3988  elopab  3992  pocl  4037  uniuni  4179  rabxfrd  4197  ontr2exmid  4246  regexmidlemm  4253  regexmidlem1  4254  preleq  4273  xpeq1  4346  elxpi  4348  vtoclr  4375  opbrop  4406  opelresg  4606  resopab2  4642  elxp4  4795  elxp5  4796  cnvpom  4847  fun11  4953  feq2  5018  f1eq2  5075  f1eq3  5076  foeq2  5090  brprcneu  5158  ssimaexg  5222  dmfco  5228  fndmdif  5259  rexsupp  5278  respreima  5282  isoeq5  5432  isoini  5444  isopolem  5448  f1oiso  5452  f1oiso2  5453  riotaeqdv  5456  acexmidlemab  5493  acexmidlemcase  5494  oprabid  5524  mpt2eq123  5551  mpt2eq123dva  5553  eloprabga  5578  resoprab  5584  resoprab2  5585  ov  5607  ovi3  5624  ov6g  5625  ovg  5626  caoftrn  5723  opabex3d  5735  opabex3  5736  elxp7  5784  eloprabi  5809  cnvf1o  5833  xporderlem  5839  poxp  5840  smoel2  5905  frec0g  5970  frecsuclem3  5977  frecsuc  5978  nnaordex  6087  qliftel  6173  brecop  6183  eroveu  6184  ecopovtrn  6190  ecopovtrng  6193  th3qlem2  6196  th3q  6198  dom2lem  6239  xpsnen  6282  xpassen  6291  dfplpq2  6433  dfmpq2  6434  ltsonq  6477  enq0sym  6511  enq0ref  6512  enq0tr  6513  enq0breq  6515  addnq0mo  6526  mulnq0mo  6527  addnnnq0  6528  mulnnnq0  6529  elinp  6553  prnmaxl  6567  prnminu  6568  prarloclemlo  6573  prarloc  6582  genpdflem  6586  genpassl  6603  genpassu  6604  ltexprlemm  6679  recexprlemell  6701  recexprlemelu  6702  cauappcvgprlemdisj  6730  caucvgprlemnkj  6745  caucvgprprlemnkltj  6768  caucvgprprlemnkeqj  6769  addsrmo  6809  mulsrmo  6810  addsrpr  6811  mulsrpr  6812  lttrsr  6828  mulgt0sr  6843  ltresr  6896  axpre-lttrn  6939  axpre-mulgt0  6942  recexgt0  7547  apreap  7554  apreim  7570  prime  8309  rexuz  8495  ltxr  8662  ixxval  8732  fzval  8843  sqrtrval  9476  abslt  9562  absle  9563  lenegsq  9569  abs2difabs  9582  2clim  9699  climcn2  9707  addcn2  9708  mulcn2  9710  climrecvg1n  9744  sumeq1  9751  bdsep2  9879  bdzfauscl  9883  bj-d0clsepcl  9922
  Copyright terms: Public domain W3C validator