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  571  pm5.71dc  903  xorbi1d  1313  drsb1  1722  ax11ev  1751  eleq1w  2143  eleq1  2145  rexeqf  2552  reueq1f  2553  rmoeq1f  2554  rabeqf  2602  vtocl2gaf  2676  alexeq  2731  ceqex  2732  elrabi  2756  sbc5  2849  rexss  3072  ineq1  3178  difin2  3244  r19.28m  3352  preq12bg  3591  opeq1  3596  eluni  3630  mpteq12f  3884  axsep2  3923  zfauscl  3924  opthg  4028  copsexg  4034  euotd  4044  elopab  4048  pocl  4093  uniuni  4236  rabxfrd  4254  ontr2exmid  4303  regexmidlemm  4310  regexmidlem1  4311  reg2exmidlema  4312  preleq  4333  xpeq1  4413  elxpi  4415  vtoclr  4442  opbrop  4473  opelresg  4676  resopab2  4714  elxp4  4870  elxp5  4871  cnvpom  4925  fun11  5032  feq2  5097  f1eq2  5158  f1eq3  5159  foeq2  5176  brprcneu  5244  ssimaexg  5309  dmfco  5315  fndmdif  5347  rexsupp  5366  respreima  5370  isoeq5  5522  isoini  5534  isopolem  5538  f1oiso  5542  f1oiso2  5543  riotaeqdv  5546  acexmidlemab  5583  acexmidlemcase  5584  oprabid  5614  mpt2eq123  5641  mpt2eq123dva  5643  eloprabga  5668  resoprab  5674  resoprab2  5675  ov  5697  ovi3  5714  ov6g  5715  ovg  5716  caoftrn  5813  opabex3d  5825  opabex3  5826  elxp7  5874  eloprabi  5899  cnvf1o  5923  xporderlem  5929  poxp  5930  smoel2  5998  frec0g  6092  freccllem  6097  frecfcllem  6099  frecsuclem  6101  frecsuc  6102  nnaordex  6214  qliftel  6300  brecop  6310  eroveu  6311  ecopovtrn  6317  ecopovtrng  6320  th3qlem2  6323  th3q  6325  dom2lem  6417  xpsnen  6465  xpassen  6474  xpf1o  6488  dfplpq2  6814  dfmpq2  6815  ltsonq  6858  enq0sym  6892  enq0ref  6893  enq0tr  6894  enq0breq  6896  addnq0mo  6907  mulnq0mo  6908  addnnnq0  6909  mulnnnq0  6910  elinp  6934  prnmaxl  6948  prnminu  6949  prarloclemlo  6954  prarloc  6963  genpdflem  6967  genpassl  6984  genpassu  6985  ltexprlemm  7060  recexprlemell  7082  recexprlemelu  7083  cauappcvgprlemdisj  7111  caucvgprlemnkj  7126  caucvgprprlemnkltj  7149  caucvgprprlemnkeqj  7150  addsrmo  7190  mulsrmo  7191  addsrpr  7192  mulsrpr  7193  lttrsr  7209  mulgt0sr  7224  ltresr  7277  axpre-lttrn  7320  axpre-mulgt0  7323  recexgt0  7955  apreap  7962  apreim  7978  prime  8739  rexuz  8961  ltxr  9139  ixxval  9207  fzval  9319  sqrtrval  10258  abslt  10346  absle  10347  lenegsq  10353  abs2difabs  10366  2clim  10512  climcn2  10520  addcn2  10521  mulcn2  10523  climrecvg1n  10557  sumeq1  10564  nndivdvds  10580  divalg2  10704  gcdval  10729  bezoutlemstep  10764  bezoutlemmain  10765  bezoutlemex  10768  gcdass  10782  lcmval  10823  lcmass  10845  rpexp  10910  bdsep2  11118  bdzfauscl  11122  bj-d0clsepcl  11161
  Copyright terms: Public domain W3C validator