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

Theorem bi2anan9 571
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 453 . 2  |-  ( ph  ->  ( ( ps  /\  ta )  <->  ( ch  /\  ta ) ) )
3 bi2an9.2 . . 3  |-  ( th 
->  ( ta  <->  et )
)
43anbi2d 452 . 2  |-  ( th 
->  ( ( ch  /\  ta )  <->  ( ch  /\  et ) ) )
52, 4sylan9bb 450 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  <->  ( ch  /\  et ) ) )
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:  bi2anan9r  572  rspc2gv  2720  ralprg  3461  raltpg  3463  prssg  3562  prsspwg  3564  opelopab2a  4048  opelxp  4420  eqrel  4475  eqrelrel  4487  brcog  4550  dff13  5459  resoprab2  5649  ovig  5673  dfoprab4f  5870  f1o2ndf1  5900  eroveu  6284  th3qlem1  6295  th3qlem2  6296  th3q  6298  oviec  6299  endisj  6389  dfplpq2  6658  dfmpq2  6659  ordpipqqs  6678  enq0enq  6735  mulnnnq0  6754  ltsrprg  7038  axcnre  7161  axmulgt0  7303  addltmul  8386  ltxr  8979  sumsqeq0  9703  dvds2lem  10415  opoe  10502  omoe  10503  opeo  10504  omeo  10505  gcddvds  10562  dfgcd2  10610
  Copyright terms: Public domain W3C validator