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

Theorem anbi1d 438
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 424 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  anbi1  439  anbi12d  442  bi2anan9  538  pm5.71dc  868  xorbi1d  1272  drsb1  1680  ax11ev  1709  eleq1  2100  rexeqf  2499  reueq1f  2500  rmoeq1f  2501  rabeqf  2547  vtocl2gaf  2617  alexeq  2667  ceqex  2668  elrabi  2692  sbc5  2784  rexss  3004  psstr  3046  sspsstr  3047  ineq1  3128  difin2  3196  r19.28m  3308  preq12bg  3541  opeq1  3546  eluni  3580  mpteq12f  3834  axsep2  3873  zfauscl  3874  opthg  3972  copsexg  3978  euotd  3988  elopab  3992  pocl  4037  uniuni  4170  rabxfrd  4188  ontr2exmid  4237  regexmidlemm  4244  regexmidlem1  4245  preleq  4264  xpeq1  4337  elxpi  4339  vtoclr  4366  opbrop  4397  opelresg  4597  resopab2  4633  elxp4  4786  elxp5  4787  cnvpom  4838  fun11  4944  feq2  5009  f1eq2  5066  f1eq3  5067  foeq2  5081  brprcneu  5149  ssimaexg  5213  dmfco  5219  fndmdif  5250  rexsupp  5269  respreima  5273  isoeq5  5423  isoini  5435  isopolem  5439  f1oiso  5443  f1oiso2  5444  riotaeqdv  5447  acexmidlemab  5484  acexmidlemcase  5485  oprabid  5515  mpt2eq123  5542  mpt2eq123dva  5544  eloprabga  5569  resoprab  5575  resoprab2  5576  ov  5598  ovi3  5615  ov6g  5616  ovg  5617  caoftrn  5714  opabex3d  5726  opabex3  5727  elxp7  5775  eloprabi  5800  cnvf1o  5824  xporderlem  5830  poxp  5831  smoel2  5896  frec0g  5961  frecsuclem3  5968  frecsuc  5969  nnaordex  6078  qliftel  6164  brecop  6174  eroveu  6175  ecopovtrn  6181  ecopovtrng  6184  th3qlem2  6187  th3q  6189  dom2lem  6230  xpsnen  6273  xpassen  6282  dfplpq2  6424  dfmpq2  6425  ltsonq  6468  enq0sym  6502  enq0ref  6503  enq0tr  6504  enq0breq  6506  addnq0mo  6517  mulnq0mo  6518  addnnnq0  6519  mulnnnq0  6520  elinp  6544  prnmaxl  6558  prnminu  6559  prarloclemlo  6564  prarloc  6573  genpdflem  6577  genpassl  6594  genpassu  6595  ltexprlemm  6670  recexprlemell  6692  recexprlemelu  6693  cauappcvgprlemdisj  6721  caucvgprlemnkj  6736  caucvgprprlemnkltj  6759  caucvgprprlemnkeqj  6760  addsrmo  6800  mulsrmo  6801  addsrpr  6802  mulsrpr  6803  lttrsr  6819  mulgt0sr  6834  ltresr  6887  axpre-lttrn  6930  axpre-mulgt0  6933  recexgt0  7538  apreap  7545  apreim  7561  prime  8300  rexuz  8486  ltxr  8653  ixxval  8723  fzval  8834  sqrtrval  9467  abslt  9553  absle  9554  lenegsq  9560  abs2difabs  9573  2clim  9690  climcn2  9698  addcn2  9699  mulcn2  9701  climrecvg1n  9735  sumeq1  9742  bdsep2  9870  bdzfauscl  9874  bj-d0clsepcl  9913
  Copyright terms: Public domain W3C validator