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

Theorem bi2anan9 580
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  581  rspc2gv  2775  ralprg  3544  raltpg  3546  prssg  3647  prsspwg  3649  opelopab2a  4157  opelxp  4539  eqrel  4598  eqrelrel  4610  brcog  4676  dff13  5637  resoprab2  5836  ovig  5860  dfoprab4f  6059  f1o2ndf1  6093  eroveu  6488  th3qlem1  6499  th3qlem2  6500  th3q  6502  oviec  6503  endisj  6686  dfplpq2  7130  dfmpq2  7131  ordpipqqs  7150  enq0enq  7207  mulnnnq0  7226  ltsrprg  7523  axcnre  7657  axmulgt0  7804  addltmul  8914  ltxr  9517  sumsqeq0  10326  mul0inf  10967  dvds2lem  11417  opoe  11504  omoe  11505  opeo  11506  omeo  11507  gcddvds  11564  dfgcd2  11614  txbasval  12347  cnmpt12  12367  cnmpt22  12374
  Copyright terms: Public domain W3C validator