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

Theorem anbi1d 453
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 439 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:  anbi1  454  anbi12d  457  bi2anan9  571  pm5.71dc  903  xorbi1d  1313  drsb1  1721  ax11ev  1750  eleq1  2142  rexeqf  2547  reueq1f  2548  rmoeq1f  2549  rabeqf  2595  vtocl2gaf  2666  alexeq  2722  ceqex  2723  elrabi  2747  sbc5  2839  rexss  3062  ineq1  3161  difin2  3227  r19.28m  3332  preq12bg  3567  opeq1  3572  eluni  3606  mpteq12f  3860  axsep2  3899  zfauscl  3900  opthg  3995  copsexg  4001  euotd  4011  elopab  4015  pocl  4060  uniuni  4203  rabxfrd  4221  ontr2exmid  4270  regexmidlemm  4277  regexmidlem1  4278  reg2exmidlema  4279  preleq  4300  xpeq1  4379  elxpi  4381  vtoclr  4408  opbrop  4439  opelresg  4641  resopab2  4679  elxp4  4832  elxp5  4833  cnvpom  4884  fun11  4991  feq2  5056  f1eq2  5113  f1eq3  5114  foeq2  5128  brprcneu  5196  ssimaexg  5261  dmfco  5267  fndmdif  5298  rexsupp  5317  respreima  5321  isoeq5  5470  isoini  5482  isopolem  5486  f1oiso  5490  f1oiso2  5491  riotaeqdv  5494  acexmidlemab  5531  acexmidlemcase  5532  oprabid  5562  mpt2eq123  5589  mpt2eq123dva  5591  eloprabga  5616  resoprab  5622  resoprab2  5623  ov  5645  ovi3  5662  ov6g  5663  ovg  5664  caoftrn  5761  opabex3d  5773  opabex3  5774  elxp7  5822  eloprabi  5847  cnvf1o  5871  xporderlem  5877  poxp  5878  smoel2  5946  frec0g  6040  freccllem  6045  frecfcllem  6047  frecsuclem  6049  frecsuc  6050  nnaordex  6159  qliftel  6245  brecop  6255  eroveu  6256  ecopovtrn  6262  ecopovtrng  6265  th3qlem2  6268  th3q  6270  dom2lem  6311  xpsnen  6355  xpassen  6364  xpf1o  6375  dfplpq2  6595  dfmpq2  6596  ltsonq  6639  enq0sym  6673  enq0ref  6674  enq0tr  6675  enq0breq  6677  addnq0mo  6688  mulnq0mo  6689  addnnnq0  6690  mulnnnq0  6691  elinp  6715  prnmaxl  6729  prnminu  6730  prarloclemlo  6735  prarloc  6744  genpdflem  6748  genpassl  6765  genpassu  6766  ltexprlemm  6841  recexprlemell  6863  recexprlemelu  6864  cauappcvgprlemdisj  6892  caucvgprlemnkj  6907  caucvgprprlemnkltj  6930  caucvgprprlemnkeqj  6931  addsrmo  6971  mulsrmo  6972  addsrpr  6973  mulsrpr  6974  lttrsr  6990  mulgt0sr  7005  ltresr  7058  axpre-lttrn  7101  axpre-mulgt0  7104  recexgt0  7736  apreap  7743  apreim  7759  prime  8516  rexuz  8738  ltxr  8916  ixxval  8984  fzval  9096  sqrtrval  10013  abslt  10101  absle  10102  lenegsq  10108  abs2difabs  10121  2clim  10267  climcn2  10275  addcn2  10276  mulcn2  10278  climrecvg1n  10312  sumeq1  10319  nndivdvds  10335  divalg2  10459  gcdval  10484  bezoutlemstep  10519  bezoutlemmain  10520  bezoutlemex  10523  gcdass  10537  lcmval  10578  lcmass  10600  rpexp  10665  bdsep2  10820  bdzfauscl  10824  bj-d0clsepcl  10863
  Copyright terms: Public domain W3C validator