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

Theorem bi2anan9 596
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
Hypotheses
Ref Expression
bi2an9.1 (𝜑 → (𝜓𝜒))
bi2an9.2 (𝜃 → (𝜏𝜂))
Assertion
Ref Expression
bi2anan9 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))

Proof of Theorem bi2anan9
StepHypRef Expression
1 bi2an9.1 . . 3 (𝜑 → (𝜓𝜒))
21anbi1d 461 . 2 (𝜑 → ((𝜓𝜏) ↔ (𝜒𝜏)))
3 bi2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43anbi2d 460 . 2 (𝜃 → ((𝜒𝜏) ↔ (𝜒𝜂)))
52, 4sylan9bb 458 1 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
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  597  rspc2gv  2805  ralprg  3582  raltpg  3584  prssg  3685  prsspwg  3687  opelopab2a  4195  opelxp  4577  eqrel  4636  eqrelrel  4648  brcog  4714  dff13  5677  resoprab2  5876  ovig  5900  dfoprab4f  6099  f1o2ndf1  6133  eroveu  6528  th3qlem1  6539  th3qlem2  6540  th3q  6542  oviec  6543  endisj  6726  dfplpq2  7186  dfmpq2  7187  ordpipqqs  7206  enq0enq  7263  mulnnnq0  7282  ltsrprg  7579  axcnre  7713  axmulgt0  7860  addltmul  8980  ltxr  9592  sumsqeq0  10402  mul0inf  11044  dvds2lem  11541  opoe  11628  omoe  11629  opeo  11630  omeo  11631  gcddvds  11688  dfgcd2  11738  txbasval  12475  cnmpt12  12495  cnmpt22  12502
  Copyright terms: Public domain W3C validator