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

Theorem anbi1d 446
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 432 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  anbi1  447  anbi12d  450  bi2anan9  548  pm5.71dc  879  xorbi1d  1288  drsb1  1696  ax11ev  1725  eleq1  2116  rexeqf  2519  reueq1f  2520  rmoeq1f  2521  rabeqf  2567  vtocl2gaf  2637  alexeq  2692  ceqex  2693  elrabi  2717  sbc5  2809  rexss  3034  psstr  3076  sspsstr  3077  ineq1  3158  difin2  3226  r19.28m  3338  preq12bg  3571  opeq1  3576  eluni  3610  mpteq12f  3864  axsep2  3903  zfauscl  3904  opthg  4002  copsexg  4008  euotd  4018  elopab  4022  pocl  4067  uniuni  4210  rabxfrd  4228  ontr2exmid  4277  regexmidlemm  4284  regexmidlem1  4285  reg2exmidlema  4286  preleq  4306  xpeq1  4386  elxpi  4388  vtoclr  4415  opbrop  4446  opelresg  4646  resopab2  4682  elxp4  4835  elxp5  4836  cnvpom  4887  fun11  4993  feq2  5058  f1eq2  5115  f1eq3  5116  foeq2  5130  brprcneu  5198  ssimaexg  5262  dmfco  5268  fndmdif  5299  rexsupp  5318  respreima  5322  isoeq5  5472  isoini  5484  isopolem  5488  f1oiso  5492  f1oiso2  5493  riotaeqdv  5496  acexmidlemab  5533  acexmidlemcase  5534  oprabid  5564  mpt2eq123  5591  mpt2eq123dva  5593  eloprabga  5618  resoprab  5624  resoprab2  5625  ov  5647  ovi3  5664  ov6g  5665  ovg  5666  caoftrn  5763  opabex3d  5775  opabex3  5776  elxp7  5824  eloprabi  5849  cnvf1o  5873  xporderlem  5879  poxp  5880  smoel2  5948  frec0g  6013  frecsuclem3  6020  frecsuc  6021  nnaordex  6130  qliftel  6216  brecop  6226  eroveu  6227  ecopovtrn  6233  ecopovtrng  6236  th3qlem2  6239  th3q  6241  dom2lem  6282  xpsnen  6325  xpassen  6334  dfplpq2  6509  dfmpq2  6510  ltsonq  6553  enq0sym  6587  enq0ref  6588  enq0tr  6589  enq0breq  6591  addnq0mo  6602  mulnq0mo  6603  addnnnq0  6604  mulnnnq0  6605  elinp  6629  prnmaxl  6643  prnminu  6644  prarloclemlo  6649  prarloc  6658  genpdflem  6662  genpassl  6679  genpassu  6680  ltexprlemm  6755  recexprlemell  6777  recexprlemelu  6778  cauappcvgprlemdisj  6806  caucvgprlemnkj  6821  caucvgprprlemnkltj  6844  caucvgprprlemnkeqj  6845  addsrmo  6885  mulsrmo  6886  addsrpr  6887  mulsrpr  6888  lttrsr  6904  mulgt0sr  6919  ltresr  6972  axpre-lttrn  7015  axpre-mulgt0  7018  recexgt0  7644  apreap  7651  apreim  7667  prime  8395  rexuz  8618  ltxr  8795  ixxval  8865  fzval  8977  sqrtrval  9826  abslt  9914  absle  9915  lenegsq  9921  abs2difabs  9934  2clim  10052  climcn2  10060  addcn2  10061  mulcn2  10063  climrecvg1n  10097  sumeq1  10104  nndivdvds  10113  bdsep2  10372  bdzfauscl  10376  bj-d0clsepcl  10415
  Copyright terms: Public domain W3C validator