ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi1d Unicode 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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
anbi1d  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )

Proof of Theorem anbi1d
StepHypRef Expression
1 anbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 22 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 439 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
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  573  pm5.71dc  907  xorbi1d  1317  drsb1  1727  ax11ev  1756  eleq1w  2148  eleq1  2150  rexeqf  2559  reueq1f  2560  rmoeq1f  2561  rabeqf  2609  vtocl2gaf  2686  alexeq  2741  ceqex  2742  elrabi  2766  sbc5  2861  rexss  3086  ineq1  3192  difin2  3259  r19.28m  3367  preq12bg  3612  opeq1  3617  eluni  3651  disjiun  3832  mpteq12f  3910  axsep2  3950  zfauscl  3951  opthg  4056  copsexg  4062  euotd  4072  elopab  4076  pocl  4121  uniuni  4264  rabxfrd  4282  ontr2exmid  4331  regexmidlemm  4338  regexmidlem1  4339  reg2exmidlema  4340  preleq  4361  xpeq1  4442  elxpi  4444  vtoclr  4474  opbrop  4505  opelresg  4708  resopab2  4746  elxp4  4905  elxp5  4906  cnvpom  4960  fun11  5067  feq2  5132  f1eq2  5196  f1eq3  5197  foeq2  5214  brprcneu  5282  ssimaexg  5350  dmfco  5356  fndmdif  5388  rexsupp  5407  respreima  5411  isoeq5  5566  isoini  5579  isopolem  5583  f1oiso  5587  f1oiso2  5588  riotaeqdv  5591  acexmidlemab  5628  acexmidlemcase  5629  oprabid  5663  mpt2eq123  5690  mpt2eq123dva  5692  eloprabga  5717  resoprab  5723  resoprab2  5724  ov  5746  ovi3  5763  ov6g  5764  ovg  5765  caoftrn  5862  opabex3d  5874  opabex3  5875  elxp7  5923  eloprabi  5948  cnvf1o  5972  xporderlem  5978  poxp  5979  smoel2  6050  frec0g  6144  freccllem  6149  frecfcllem  6151  frecsuclem  6153  frecsuc  6154  nnaordex  6266  qliftel  6352  brecop  6362  eroveu  6363  ecopovtrn  6369  ecopovtrng  6372  th3qlem2  6375  th3q  6377  dom2lem  6469  xpsnen  6517  xpassen  6526  xpf1o  6540  dfplpq2  6892  dfmpq2  6893  ltsonq  6936  enq0sym  6970  enq0ref  6971  enq0tr  6972  enq0breq  6974  addnq0mo  6985  mulnq0mo  6986  addnnnq0  6987  mulnnnq0  6988  elinp  7012  prnmaxl  7026  prnminu  7027  prarloclemlo  7032  prarloc  7041  genpdflem  7045  genpassl  7062  genpassu  7063  ltexprlemm  7138  recexprlemell  7160  recexprlemelu  7161  cauappcvgprlemdisj  7189  caucvgprlemnkj  7204  caucvgprprlemnkltj  7227  caucvgprprlemnkeqj  7228  addsrmo  7268  mulsrmo  7269  addsrpr  7270  mulsrpr  7271  lttrsr  7287  mulgt0sr  7302  ltresr  7355  axpre-lttrn  7398  axpre-mulgt0  7401  recexgt0  8033  apreap  8040  apreim  8056  prime  8815  rexuz  9037  ltxr  9215  ixxval  9283  fzval  9395  sqrtrval  10398  abslt  10486  absle  10487  lenegsq  10493  abs2difabs  10506  2clim  10653  climcn2  10662  addcn2  10663  mulcn2  10665  climrecvg1n  10701  sumeq1  10708  fsum2dlemstep  10791  modfsummod  10815  nndivdvds  10895  divalg2  11019  gcdval  11044  bezoutlemstep  11079  bezoutlemmain  11080  bezoutlemex  11083  gcdass  11097  lcmval  11138  lcmass  11160  rpexp  11225  bdsep2  11434  bdzfauscl  11438  bj-d0clsepcl  11477
  Copyright terms: Public domain W3C validator