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

Theorem bi2anan9 595
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
Hypotheses
Ref Expression
bi2an9.1  |-  ( ph  ->  ( ps  <->  ch )
)
bi2an9.2  |-  ( th 
->  ( ta  <->  et )
)
Assertion
Ref Expression
bi2anan9  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  <->  ( ch  /\  et ) ) )

Proof of Theorem bi2anan9
StepHypRef Expression
1 bi2an9.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21anbi1d 460 . 2  |-  ( ph  ->  ( ( ps  /\  ta )  <->  ( ch  /\  ta ) ) )
3 bi2an9.2 . . 3  |-  ( th 
->  ( ta  <->  et )
)
43anbi2d 459 . 2  |-  ( th 
->  ( ( ch  /\  ta )  <->  ( ch  /\  et ) ) )
52, 4sylan9bb 457 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  <->  ( ch  /\  et ) ) )
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:  bi2anan9r  596  rspc2gv  2801  ralprg  3577  raltpg  3579  prssg  3680  prsspwg  3682  opelopab2a  4190  opelxp  4572  eqrel  4631  eqrelrel  4643  brcog  4709  dff13  5672  resoprab2  5871  ovig  5895  dfoprab4f  6094  f1o2ndf1  6128  eroveu  6523  th3qlem1  6534  th3qlem2  6535  th3q  6537  oviec  6538  endisj  6721  dfplpq2  7181  dfmpq2  7182  ordpipqqs  7201  enq0enq  7258  mulnnnq0  7277  ltsrprg  7574  axcnre  7708  axmulgt0  7855  addltmul  8975  ltxr  9585  sumsqeq0  10395  mul0inf  11036  dvds2lem  11528  opoe  11615  omoe  11616  opeo  11617  omeo  11618  gcddvds  11675  dfgcd2  11725  txbasval  12462  cnmpt12  12482  cnmpt22  12489
  Copyright terms: Public domain W3C validator