ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi1d Structured version   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  867  xorbi1d  1270  drsb1  1677  ax11ev  1706  eleq1  2097  rexeqf  2496  reueq1f  2497  rmoeq1f  2498  rabeqf  2544  vtocl2gaf  2614  alexeq  2664  ceqex  2665  elrabi  2689  sbc5  2781  rexss  3001  psstr  3043  sspsstr  3044  ineq1  3125  difin2  3193  r19.28m  3305  preq12bg  3535  opeq1  3540  eluni  3574  mpteq12f  3828  axsep2  3867  zfauscl  3868  opthg  3966  copsexg  3972  euotd  3982  elopab  3986  pocl  4031  uniuni  4149  rabxfrd  4167  regexmidlemm  4217  regexmidlem1  4218  preleq  4233  xpeq1  4302  elxpi  4304  vtoclr  4331  opbrop  4362  opelresg  4562  resopab2  4598  elxp4  4751  elxp5  4752  cnvpom  4803  fun11  4909  feq2  4974  f1eq2  5031  f1eq3  5032  foeq2  5046  brprcneu  5114  ssimaexg  5178  dmfco  5184  fndmdif  5215  rexsupp  5234  respreima  5238  isoeq5  5388  isoini  5400  isopolem  5404  f1oiso  5408  f1oiso2  5409  riotaeqdv  5412  acexmidlemab  5449  acexmidlemcase  5450  oprabid  5480  mpt2eq123  5506  mpt2eq123dva  5508  eloprabga  5533  resoprab  5539  resoprab2  5540  ov  5562  ovi3  5579  ov6g  5580  ovg  5581  caoftrn  5678  opabex3d  5690  opabex3  5691  elxp7  5739  eloprabi  5764  cnvf1o  5788  xporderlem  5793  poxp  5794  smoel2  5859  frec0g  5922  frecsuclem3  5929  frecsuc  5930  nnaordex  6036  qliftel  6122  brecop  6132  eroveu  6133  ecopovtrn  6139  ecopovtrng  6142  th3qlem2  6145  th3q  6147  dom2lem  6188  xpsnen  6231  xpassen  6240  dfplpq2  6338  dfmpq2  6339  ltsonq  6382  enq0sym  6414  enq0ref  6415  enq0tr  6416  enq0breq  6418  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  mulnnnq0  6432  elinp  6456  prnmaxl  6470  prnminu  6471  prarloclemlo  6476  prarloc  6485  genpdflem  6489  genpassl  6507  genpassu  6508  ltexprlemm  6572  recexprlemell  6592  recexprlemelu  6593  addsrmo  6631  mulsrmo  6632  addsrpr  6633  mulsrpr  6634  lttrsr  6650  mulgt0sr  6664  ltresr  6696  axpre-lttrn  6728  axpre-mulgt0  6731  recexgt0  7324  apreap  7331  apreim  7347  prime  8073  rexuz  8259  ltxr  8425  ixxval  8495  fzval  8606  bdsep2  9274  bdzfauscl  9278  bj-d0clsepcl  9314
  Copyright terms: Public domain W3C validator