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  2502  reueq1f  2503  rmoeq1f  2504  rabeqf  2550  vtocl2gaf  2620  alexeq  2670  ceqex  2671  elrabi  2695  sbc5  2787  rexss  3007  psstr  3049  sspsstr  3050  ineq1  3131  difin2  3199  r19.28m  3311  preq12bg  3544  opeq1  3549  eluni  3583  mpteq12f  3837  axsep2  3876  zfauscl  3877  opthg  3975  copsexg  3981  euotd  3991  elopab  3995  pocl  4040  uniuni  4183  rabxfrd  4201  ontr2exmid  4250  regexmidlemm  4257  regexmidlem1  4258  reg2exmidlema  4259  preleq  4279  xpeq1  4359  elxpi  4361  vtoclr  4388  opbrop  4419  opelresg  4619  resopab2  4655  elxp4  4808  elxp5  4809  cnvpom  4860  fun11  4966  feq2  5031  f1eq2  5088  f1eq3  5089  foeq2  5103  brprcneu  5171  ssimaexg  5235  dmfco  5241  fndmdif  5272  rexsupp  5291  respreima  5295  isoeq5  5445  isoini  5457  isopolem  5461  f1oiso  5465  f1oiso2  5466  riotaeqdv  5469  acexmidlemab  5506  acexmidlemcase  5507  oprabid  5537  mpt2eq123  5564  mpt2eq123dva  5566  eloprabga  5591  resoprab  5597  resoprab2  5598  ov  5620  ovi3  5637  ov6g  5638  ovg  5639  caoftrn  5736  opabex3d  5748  opabex3  5749  elxp7  5797  eloprabi  5822  cnvf1o  5846  xporderlem  5852  poxp  5853  smoel2  5918  frec0g  5983  frecsuclem3  5990  frecsuc  5991  nnaordex  6100  qliftel  6186  brecop  6196  eroveu  6197  ecopovtrn  6203  ecopovtrng  6206  th3qlem2  6209  th3q  6211  dom2lem  6252  xpsnen  6295  xpassen  6304  dfplpq2  6450  dfmpq2  6451  ltsonq  6494  enq0sym  6528  enq0ref  6529  enq0tr  6530  enq0breq  6532  addnq0mo  6543  mulnq0mo  6544  addnnnq0  6545  mulnnnq0  6546  elinp  6570  prnmaxl  6584  prnminu  6585  prarloclemlo  6590  prarloc  6599  genpdflem  6603  genpassl  6620  genpassu  6621  ltexprlemm  6696  recexprlemell  6718  recexprlemelu  6719  cauappcvgprlemdisj  6747  caucvgprlemnkj  6762  caucvgprprlemnkltj  6785  caucvgprprlemnkeqj  6786  addsrmo  6826  mulsrmo  6827  addsrpr  6828  mulsrpr  6829  lttrsr  6845  mulgt0sr  6860  ltresr  6913  axpre-lttrn  6956  axpre-mulgt0  6959  recexgt0  7569  apreap  7576  apreim  7592  prime  8335  rexuz  8521  ltxr  8693  ixxval  8763  fzval  8874  sqrtrval  9596  abslt  9682  absle  9683  lenegsq  9689  abs2difabs  9702  2clim  9820  climcn2  9828  addcn2  9829  mulcn2  9831  climrecvg1n  9865  sumeq1  9872  bdsep2  10004  bdzfauscl  10008  bj-d0clsepcl  10047
  Copyright terms: Public domain W3C validator