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

Theorem anbi2d 445
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 431 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
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:  anbi2  448  anbi12d  450  bi2anan9  546  dn1dc  876  xorbi2d  1285  dfbi3dc  1302  xordidc  1304  eleq2  2115  ceqsex2  2609  ceqsex6v  2613  vtocl2gaf  2635  ceqsrex2v  2696  mob2  2741  eqreu  2753  nelrdva  2766  psssstr  3076  undif4  3309  r19.27m  3341  ifbi  3373  preq12bg  3569  opeq2  3575  ralunsn  3593  intab  3669  opabbid  3847  opthg  4000  pocl  4065  ordelord  4143  ordtriexmid  4272  ontr2exmid  4275  onsucsssucexmid  4277  tfisi  4335  xpeq2  4385  rabxp  4405  vtoclr  4413  opeliunxp  4420  posng  4437  opbrop  4444  rexiunxp  4503  elrnmpt1  4610  dfres2  4683  brcodir  4737  poltletr  4750  xp11m  4784  elxp4  4833  elxp5  4834  dffun4f  4943  fununi  4992  fneq2  5013  fnun  5030  feq3  5057  foeq3  5129  funfveu  5213  funbrfv  5237  ssimaexg  5260  fvopab3g  5270  fvopab3ig  5271  fvelrn  5323  fmptco  5355  fsn2  5362  elunirn  5430  isoeq2  5467  isoeq3  5468  isocnv2  5477  isoini  5482  isopolem  5486  f1oiso  5490  f1oiso2  5491  oprabbid  5583  cbvoprab3  5605  mpt2mptx  5620  mpt2fun  5628  ov  5645  ovi3  5662  ov6g  5663  ovg  5664  caoftrn  5761  f1o2ndf1  5874  xporderlem  5877  f1od2  5881  brtpos2  5894  brtposg  5897  dftpos4  5906  recseq  5949  tfrlem3-2  5955  tfrlem3-2d  5956  tfrlemi1  5974  tfrexlem  5976  freceq1  6007  freceq2  6008  frecsuc  6019  nnaordex  6128  brecop  6224  eroveu  6225  erovlem  6226  ecopovtrn  6231  ecopovtrng  6234  th3qlem1  6236  th3qlem2  6237  th3q  6239  domeng  6261  dom2lem  6280  xpcomco  6328  xpassen  6332  xpdom2  6333  phplem3g  6347  ssfiexmid  6364  findcard2  6374  findcard2s  6375  findcard2d  6376  findcard2sd  6377  diffifi  6379  recexnq  6516  recmulnqg  6517  ltsonq  6524  enq0sym  6558  enq0ref  6559  enq0tr  6560  enq0breq  6562  addnq0mo  6573  mulnq0mo  6574  addnnnq0  6575  mulnnnq0  6576  elinp  6600  prdisj  6618  prarloclem3  6623  prarloc  6629  distrlem5prl  6712  distrlem5pru  6713  ltexprlemell  6724  ltexprlemelu  6725  recexprlemm  6750  addsrmo  6856  mulsrmo  6857  addsrpr  6858  mulsrpr  6859  lttrsr  6875  recexgt0sr  6886  mulgt0sr  6890  ltresr  6943  axprecex  6982  axpre-lttrn  6986  axpre-mulgt0  6989  lesub0  7518  apreap  7622  apreim  7638  zltlen  8347  prime  8366  fzind  8382  qltlen  8642  xltnegi  8819  ixxval  8836  fzval  8948  fzdifsuc  9015  elfzm11  9025  elfzo  9078  qbtwnzlemshrink  9176  rebtwn2zlemshrink  9180  facwordi  9572  shftfvalg  9611  shftfibg  9613  shftfval  9614  shftfib  9616  shftfn  9617  2shfti  9624  cau3lem  9904  caubnd2  9907  clim  9996  clim2  9998  climi  10002  climcn2  10024  addcn2  10025  subcn2  10026  mulcn2  10027  pw2dvdslemn  10196  algcvgblem  10214
  Copyright terms: Public domain W3C validator