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

Theorem anbi1d 460
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 446 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
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  461  anbi12d  464  bi2anan9  580  pm5.71dc  930  xorbi1d  1344  drsb1  1755  ax11ev  1784  eleq1w  2178  eleq1  2180  rexeqf  2600  reueq1f  2601  rmoeq1f  2602  rabeqf  2650  vtocl2gaf  2727  alexeq  2785  ceqex  2786  elrabi  2810  sbc5  2905  rexss  3134  ineq1  3240  difin2  3308  r19.28m  3422  preq12bg  3670  opeq1  3675  eluni  3709  disjiun  3894  mpteq12f  3978  axsep2  4017  zfauscl  4018  opthg  4130  copsexg  4136  euotd  4146  elopab  4150  pocl  4195  uniuni  4342  rabxfrd  4360  ontr2exmid  4410  regexmidlemm  4417  regexmidlem1  4418  reg2exmidlema  4419  preleq  4440  xpeq1  4523  elxpi  4525  vtoclr  4557  opbrop  4588  opelresg  4796  resopab2  4836  elxp4  4996  elxp5  4997  cnvpom  5051  fun11  5160  feq2  5226  f1eq2  5294  f1eq3  5295  foeq2  5312  brprcneu  5382  ssimaexg  5451  dmfco  5457  fndmdif  5493  rexsupp  5512  respreima  5516  isoeq5  5674  isoini  5687  isopolem  5691  f1oiso  5695  f1oiso2  5696  riotaeqdv  5699  acexmidlemab  5736  acexmidlemcase  5737  oprabid  5771  mpoeq123  5798  mpoeq123dva  5800  eloprabga  5826  resoprab  5835  resoprab2  5836  ov  5858  ovi3  5875  ov6g  5876  ovg  5877  caoftrn  5975  opabex3d  5987  opabex3  5988  elxp7  6036  eloprabi  6062  cnvf1o  6090  xporderlem  6096  poxp  6097  smoel2  6168  frec0g  6262  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecsuc  6272  nnaordex  6391  qliftel  6477  brecop  6487  eroveu  6488  ecopovtrn  6494  ecopovtrng  6497  th3qlem2  6500  th3q  6502  ixpsnf1o  6598  dom2lem  6634  xpsnen  6683  xpassen  6692  xpf1o  6706  ctssdccl  6964  dfplpq2  7130  dfmpq2  7131  ltsonq  7174  enq0sym  7208  enq0ref  7209  enq0tr  7210  enq0breq  7212  addnq0mo  7223  mulnq0mo  7224  addnnnq0  7225  mulnnnq0  7226  elinp  7250  prnmaxl  7264  prnminu  7265  prarloclemlo  7270  prarloc  7279  genpdflem  7283  genpassl  7300  genpassu  7301  ltexprlemm  7376  recexprlemell  7398  recexprlemelu  7399  cauappcvgprlemdisj  7427  caucvgprlemnkj  7442  caucvgprprlemnkltj  7465  caucvgprprlemnkeqj  7466  addsrmo  7519  mulsrmo  7520  addsrpr  7521  mulsrpr  7522  lttrsr  7538  mulgt0sr  7554  ltresr  7615  axpre-lttrn  7660  axpre-mulgt0  7663  recexgt0  8309  apreap  8316  apreim  8332  aprcl  8375  prime  9108  rexuz  9331  ltxr  9517  ixxval  9634  fzval  9747  sqrtrval  10727  abslt  10815  absle  10816  lenegsq  10822  abs2difabs  10835  2clim  11025  climcn2  11033  addcn2  11034  mulcn2  11036  climrecvg1n  11072  sumeq1  11079  fsum2dlemstep  11158  modfsummod  11182  nndivdvds  11411  divalg2  11535  gcdval  11560  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlemex  11601  gcdass  11615  lcmval  11656  lcmass  11678  rpexp  11743  istopg  12077  basis2  12126  tg2  12140  iscld  12183  neival  12223  isnei  12224  isneip  12226  iscn  12277  cnpval  12278  iscnp  12279  txbas  12338  txdis1cn  12358  ispsmet  12403  ismet  12424  isxmet  12425  ismet2  12434  blres  12514  elmopn  12526  mopni  12562  neibl  12571  metrest  12586  elcncf  12640  mulc1cncf  12656  mulcncf  12671  limccnp2lem  12725  sincosq2sgn  12819  sincosq4sgn  12821  bdsep2  12980  bdzfauscl  12984  bj-d0clsepcl  13019
  Copyright terms: Public domain W3C validator