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

Theorem anbi1d 458
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 444 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  459  anbi12d  462  bi2anan9  578  pm5.71dc  928  xorbi1d  1342  drsb1  1753  ax11ev  1782  eleq1w  2176  eleq1  2178  rexeqf  2598  reueq1f  2599  rmoeq1f  2600  rabeqf  2648  vtocl2gaf  2725  alexeq  2783  ceqex  2784  elrabi  2808  sbc5  2903  rexss  3132  ineq1  3238  difin2  3306  r19.28m  3420  preq12bg  3668  opeq1  3673  eluni  3707  disjiun  3892  mpteq12f  3976  axsep2  4015  zfauscl  4016  opthg  4128  copsexg  4134  euotd  4144  elopab  4148  pocl  4193  uniuni  4340  rabxfrd  4358  ontr2exmid  4408  regexmidlemm  4415  regexmidlem1  4416  reg2exmidlema  4417  preleq  4438  xpeq1  4521  elxpi  4523  vtoclr  4555  opbrop  4586  opelresg  4794  resopab2  4834  elxp4  4994  elxp5  4995  cnvpom  5049  fun11  5158  feq2  5224  f1eq2  5292  f1eq3  5293  foeq2  5310  brprcneu  5380  ssimaexg  5449  dmfco  5455  fndmdif  5491  rexsupp  5510  respreima  5514  isoeq5  5672  isoini  5685  isopolem  5689  f1oiso  5693  f1oiso2  5694  riotaeqdv  5697  acexmidlemab  5734  acexmidlemcase  5735  oprabid  5769  mpoeq123  5796  mpoeq123dva  5798  eloprabga  5824  resoprab  5833  resoprab2  5834  ov  5856  ovi3  5873  ov6g  5874  ovg  5875  caoftrn  5973  opabex3d  5985  opabex3  5986  elxp7  6034  eloprabi  6060  cnvf1o  6088  xporderlem  6094  poxp  6095  smoel2  6166  frec0g  6260  freccllem  6265  frecfcllem  6267  frecsuclem  6269  frecsuc  6270  nnaordex  6389  qliftel  6475  brecop  6485  eroveu  6486  ecopovtrn  6492  ecopovtrng  6495  th3qlem2  6498  th3q  6500  ixpsnf1o  6596  dom2lem  6632  xpsnen  6681  xpassen  6690  xpf1o  6704  ctssdccl  6962  dfplpq2  7126  dfmpq2  7127  ltsonq  7170  enq0sym  7204  enq0ref  7205  enq0tr  7206  enq0breq  7208  addnq0mo  7219  mulnq0mo  7220  addnnnq0  7221  mulnnnq0  7222  elinp  7246  prnmaxl  7260  prnminu  7261  prarloclemlo  7266  prarloc  7275  genpdflem  7279  genpassl  7296  genpassu  7297  ltexprlemm  7372  recexprlemell  7394  recexprlemelu  7395  cauappcvgprlemdisj  7423  caucvgprlemnkj  7438  caucvgprprlemnkltj  7461  caucvgprprlemnkeqj  7462  addsrmo  7515  mulsrmo  7516  addsrpr  7517  mulsrpr  7518  lttrsr  7534  mulgt0sr  7550  ltresr  7611  axpre-lttrn  7656  axpre-mulgt0  7659  recexgt0  8305  apreap  8312  apreim  8328  aprcl  8371  prime  9104  rexuz  9327  ltxr  9513  ixxval  9630  fzval  9743  sqrtrval  10723  abslt  10811  absle  10812  lenegsq  10818  abs2difabs  10831  2clim  11021  climcn2  11029  addcn2  11030  mulcn2  11032  climrecvg1n  11068  sumeq1  11075  fsum2dlemstep  11154  modfsummod  11178  nndivdvds  11406  divalg2  11530  gcdval  11555  bezoutlemstep  11592  bezoutlemmain  11593  bezoutlemex  11596  gcdass  11610  lcmval  11651  lcmass  11673  rpexp  11738  istopg  12072  basis2  12121  tg2  12135  iscld  12178  neival  12218  isnei  12219  isneip  12221  iscn  12272  cnpval  12273  iscnp  12274  txbas  12333  txdis1cn  12353  ispsmet  12398  ismet  12419  isxmet  12420  ismet2  12429  blres  12509  elmopn  12521  mopni  12557  neibl  12566  metrest  12581  elcncf  12635  mulc1cncf  12651  mulcncf  12666  limccnp2lem  12720  bdsep2  12918  bdzfauscl  12922  bj-d0clsepcl  12957
  Copyright terms: Public domain W3C validator