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  905  xorbi1d  1315  drsb1  1724  ax11ev  1753  eleq1w  2145  eleq1  2147  rexeqf  2555  reueq1f  2556  rmoeq1f  2557  rabeqf  2605  vtocl2gaf  2679  alexeq  2734  ceqex  2735  elrabi  2759  sbc5  2852  rexss  3077  ineq1  3183  difin2  3250  r19.28m  3358  preq12bg  3600  opeq1  3605  eluni  3639  mpteq12f  3893  axsep2  3932  zfauscl  3933  opthg  4038  copsexg  4044  euotd  4054  elopab  4058  pocl  4103  uniuni  4246  rabxfrd  4264  ontr2exmid  4313  regexmidlemm  4320  regexmidlem1  4321  reg2exmidlema  4322  preleq  4343  xpeq1  4424  elxpi  4426  vtoclr  4453  opbrop  4484  opelresg  4687  resopab2  4725  elxp4  4881  elxp5  4882  cnvpom  4936  fun11  5043  feq2  5108  f1eq2  5169  f1eq3  5170  foeq2  5187  brprcneu  5255  ssimaexg  5323  dmfco  5329  fndmdif  5361  rexsupp  5380  respreima  5384  isoeq5  5539  isoini  5552  isopolem  5556  f1oiso  5560  f1oiso2  5561  riotaeqdv  5564  acexmidlemab  5601  acexmidlemcase  5602  oprabid  5632  mpt2eq123  5659  mpt2eq123dva  5661  eloprabga  5686  resoprab  5692  resoprab2  5693  ov  5715  ovi3  5732  ov6g  5733  ovg  5734  caoftrn  5831  opabex3d  5843  opabex3  5844  elxp7  5892  eloprabi  5917  cnvf1o  5941  xporderlem  5947  poxp  5948  smoel2  6016  frec0g  6110  freccllem  6115  frecfcllem  6117  frecsuclem  6119  frecsuc  6120  nnaordex  6232  qliftel  6318  brecop  6328  eroveu  6329  ecopovtrn  6335  ecopovtrng  6338  th3qlem2  6341  th3q  6343  dom2lem  6435  xpsnen  6483  xpassen  6492  xpf1o  6506  dfplpq2  6850  dfmpq2  6851  ltsonq  6894  enq0sym  6928  enq0ref  6929  enq0tr  6930  enq0breq  6932  addnq0mo  6943  mulnq0mo  6944  addnnnq0  6945  mulnnnq0  6946  elinp  6970  prnmaxl  6984  prnminu  6985  prarloclemlo  6990  prarloc  6999  genpdflem  7003  genpassl  7020  genpassu  7021  ltexprlemm  7096  recexprlemell  7118  recexprlemelu  7119  cauappcvgprlemdisj  7147  caucvgprlemnkj  7162  caucvgprprlemnkltj  7185  caucvgprprlemnkeqj  7186  addsrmo  7226  mulsrmo  7227  addsrpr  7228  mulsrpr  7229  lttrsr  7245  mulgt0sr  7260  ltresr  7313  axpre-lttrn  7356  axpre-mulgt0  7359  recexgt0  7991  apreap  7998  apreim  8014  prime  8771  rexuz  8993  ltxr  9171  ixxval  9239  fzval  9351  sqrtrval  10321  abslt  10409  absle  10410  lenegsq  10416  abs2difabs  10429  2clim  10575  climcn2  10583  addcn2  10584  mulcn2  10586  climrecvg1n  10620  sumeq1  10627  nndivdvds  10669  divalg2  10793  gcdval  10818  bezoutlemstep  10853  bezoutlemmain  10854  bezoutlemex  10857  gcdass  10871  lcmval  10912  lcmass  10934  rpexp  10999  bdsep2  11207  bdzfauscl  11211  bj-d0clsepcl  11250
  Copyright terms: Public domain W3C validator