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

Theorem anbi1d 461
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 447 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  anbi1  462  anbi12d  465  bi2anan9  596  pm5.71dc  946  xorbi1d  1360  drsb1  1772  ax11ev  1801  eleq1w  2201  eleq1  2203  rexeqf  2626  reueq1f  2627  rmoeq1f  2628  rabeqf  2679  vtocl2gaf  2756  alexeq  2814  ceqex  2815  elrabi  2840  sbc5  2935  rexss  3168  ineq1  3274  difin2  3342  r19.28m  3456  preq12bg  3707  opeq1  3712  eluni  3746  disjiun  3931  mpteq12f  4015  axsep2  4054  zfauscl  4055  opthg  4167  copsexg  4173  euotd  4183  elopab  4187  pocl  4232  uniuni  4379  rabxfrd  4397  ontr2exmid  4447  regexmidlemm  4454  regexmidlem1  4455  reg2exmidlema  4456  preleq  4477  xpeq1  4560  elxpi  4562  vtoclr  4594  opbrop  4625  opelresg  4833  resopab2  4873  elxp4  5033  elxp5  5034  cnvpom  5088  fun11  5197  feq2  5263  f1eq2  5331  f1eq3  5332  foeq2  5349  brprcneu  5421  ssimaexg  5490  dmfco  5496  fndmdif  5532  rexsupp  5551  respreima  5555  isoeq5  5713  isoini  5726  isopolem  5730  f1oiso  5734  f1oiso2  5735  riotaeqdv  5738  acexmidlemab  5775  acexmidlemcase  5776  oprabid  5810  mpoeq123  5837  mpoeq123dva  5839  eloprabga  5865  resoprab  5874  resoprab2  5875  ov  5897  ovi3  5914  ov6g  5915  ovg  5916  caoftrn  6014  opabex3d  6026  opabex3  6027  elxp7  6075  eloprabi  6101  cnvf1o  6129  xporderlem  6135  poxp  6136  smoel2  6207  frec0g  6301  freccllem  6306  frecfcllem  6308  frecsuclem  6310  frecsuc  6311  nnaordex  6430  qliftel  6516  brecop  6526  eroveu  6527  ecopovtrn  6533  ecopovtrng  6536  th3qlem2  6539  th3q  6541  ixpsnf1o  6637  dom2lem  6673  xpsnen  6722  xpassen  6731  xpf1o  6745  ctssdccl  7003  dfplpq2  7185  dfmpq2  7186  ltsonq  7229  enq0sym  7263  enq0ref  7264  enq0tr  7265  enq0breq  7267  addnq0mo  7278  mulnq0mo  7279  addnnnq0  7280  mulnnnq0  7281  elinp  7305  prnmaxl  7319  prnminu  7320  prarloclemlo  7325  prarloc  7334  genpdflem  7338  genpassl  7355  genpassu  7356  ltexprlemm  7431  recexprlemell  7453  recexprlemelu  7454  cauappcvgprlemdisj  7482  caucvgprlemnkj  7497  caucvgprprlemnkltj  7520  caucvgprprlemnkeqj  7521  addsrmo  7574  mulsrmo  7575  addsrpr  7576  mulsrpr  7577  lttrsr  7593  mulgt0sr  7609  ltresr  7670  axpre-lttrn  7715  axpre-mulgt0  7718  recexgt0  8365  apreap  8372  apreim  8388  aprcl  8431  prime  9173  rexuz  9401  ltxr  9591  ixxval  9708  fzval  9822  sqrtrval  10803  abslt  10891  absle  10892  lenegsq  10898  abs2difabs  10911  2clim  11101  climcn2  11109  addcn2  11110  mulcn2  11112  climrecvg1n  11148  sumeq1  11155  fsum2dlemstep  11234  modfsummod  11258  prodeq1f  11352  nndivdvds  11533  divalg2  11657  gcdval  11682  bezoutlemstep  11719  bezoutlemmain  11720  bezoutlemex  11723  gcdass  11737  lcmval  11778  lcmass  11800  rpexp  11865  istopg  12203  basis2  12252  tg2  12266  iscld  12309  neival  12349  isnei  12350  isneip  12352  iscn  12403  cnpval  12404  iscnp  12405  txbas  12464  txdis1cn  12484  ispsmet  12529  ismet  12550  isxmet  12551  ismet2  12560  blres  12640  elmopn  12652  mopni  12688  neibl  12697  metrest  12712  elcncf  12766  mulc1cncf  12782  mulcncf  12797  limccnp2lem  12851  sincosq2sgn  12954  sincosq4sgn  12956  bdsep2  13253  bdzfauscl  13257  bj-d0clsepcl  13292  sscoll2  13355
  Copyright terms: Public domain W3C validator