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

Theorem anbi2d 452
Description: Deduction adding a left 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
anbi2d  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )

Proof of Theorem anbi2d
StepHypRef Expression
1 anbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 22 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32d 438 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
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:  anbi2  455  anbi12d  457  bi2anan9  573  dn1dc  906  xorbi2d  1316  dfbi3dc  1333  xordidc  1335  eleq2w  2149  eleq2  2151  ceqsex2  2659  ceqsex6v  2663  vtocl2gaf  2686  ceqsrex2v  2747  mob2  2793  eqreu  2805  nelrdva  2820  dfss4st  3230  undif4  3342  r19.27m  3373  ifbi  3407  preq12bg  3612  opeq2  3618  ralunsn  3636  intab  3712  disjiun  3832  opabbid  3895  opthg  4056  pocl  4121  ordelord  4199  ordtriexmid  4328  ontr2exmid  4331  onsucsssucexmid  4333  tfisi  4392  xpeq2  4443  rabxp  4463  vtoclr  4474  opeliunxp  4481  posng  4498  opbrop  4505  rexiunxp  4566  elrnmpt1  4674  dfres2  4751  brcodir  4806  poltletr  4819  xp11m  4856  elxp4  4905  elxp5  4906  dffun4f  5018  fununi  5068  fneq2  5089  fnun  5106  feq3  5133  foeq3  5215  funfveu  5302  funbrfv  5327  ssimaexg  5350  fvopab3g  5361  fvopab3ig  5362  fvelrn  5414  fmptco  5448  fsn2  5455  elunirn  5527  isoeq2  5563  isoeq3  5564  isocnv2  5573  isoini  5579  isopolem  5583  f1oiso  5587  f1oiso2  5588  oprabbid  5684  cbvoprab3  5706  mpt2mptx  5721  mpt2fun  5729  ov  5746  ovi3  5763  ov6g  5764  ovg  5765  caoftrn  5862  f1o2ndf1  5975  xporderlem  5978  f1od2  5982  brtpos2  5998  brtposg  6001  dftpos4  6010  recseq  6053  tfrlem3-2d  6059  tfrlemi1  6079  tfrexlem  6081  tfr1onlemaccex  6095  tfrcllemaccex  6108  tfrcl  6111  freceq1  6139  freceq2  6140  frecsuc  6154  nnaordex  6266  brecop  6362  eroveu  6363  erovlem  6364  ecopovtrn  6369  ecopovtrng  6372  th3qlem1  6374  th3qlem2  6375  th3q  6377  elpmg  6401  domeng  6449  dom2lem  6469  xpcomco  6522  xpassen  6526  xpdom2  6527  xpf1o  6540  phplem3g  6552  ssfiexmid  6572  domfiexmid  6574  findcard2  6585  findcard2s  6586  findcard2d  6587  findcard2sd  6588  diffifi  6590  fidcenumlemrk  6642  fidcenumlemr  6643  supeq2  6663  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  recexnq  6928  recmulnqg  6929  ltsonq  6936  enq0sym  6970  enq0ref  6971  enq0tr  6972  enq0breq  6974  addnq0mo  6985  mulnq0mo  6986  addnnnq0  6987  mulnnnq0  6988  elinp  7012  prdisj  7030  prarloclem3  7035  prarloc  7041  distrlem5prl  7124  distrlem5pru  7125  ltexprlemell  7136  ltexprlemelu  7137  recexprlemm  7162  addsrmo  7268  mulsrmo  7269  addsrpr  7270  mulsrpr  7271  lttrsr  7287  recexgt0sr  7298  mulgt0sr  7302  ltresr  7355  axprecex  7394  axpre-lttrn  7398  axpre-mulgt0  7401  lesub0  7936  apreap  8040  apreim  8056  zltlen  8795  prime  8815  fzind  8831  qltlen  9094  xltnegi  9266  ixxval  9283  fzval  9395  fzdifsuc  9462  elfzm11  9472  elfzo  9525  exbtwnzlemshrink  9625  rebtwn2zlemshrink  9630  facwordi  10113  zfz1iso  10211  shftfvalg  10217  shftfibg  10219  shftfval  10220  shftfib  10222  shftfn  10223  2shfti  10230  cau3lem  10512  caubnd2  10515  clim  10633  clim2  10635  climi  10639  climcn2  10662  addcn2  10663  subcn2  10664  mulcn2  10665  isummolem2a  10735  isummo  10737  fisum  10742  fsumsplitf  10765  divalgb  11018  ndvdssub  11023  zsupcllemex  11035  gcdval  11044  gcdneg  11066  bezoutlemstep  11079  bezoutlemmain  11080  bezoutlemex  11083  dfgcd2  11096  gcdass  11097  algcvgblem  11124  lcmval  11138  lcmneg  11149  lcmgcdlem  11152  lcmass  11160  qredeq  11171  prmind2  11195  euclemma  11218  pw2dvdslemn  11236  qnumval  11256  qdenval  11257
  Copyright terms: Public domain W3C validator