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

Theorem bi2anan9 548
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 446 . 2 (𝜑 → ((𝜓𝜏) ↔ (𝜒𝜏)))
3 bi2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43anbi2d 445 . 2 (𝜃 → ((𝜒𝜏) ↔ (𝜒𝜂)))
52, 4sylan9bb 443 1 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
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:  bi2anan9r  549  ralprg  3448  raltpg  3450  prssg  3548  prsspwg  3550  opelopab2a  4029  opelxp  4401  eqrel  4456  eqrelrel  4468  brcog  4529  dff13  5434  resoprab2  5625  ovig  5649  dfoprab4f  5846  f1o2ndf1  5876  eroveu  6227  th3qlem1  6238  th3qlem2  6239  th3q  6241  oviec  6242  endisj  6328  dfplpq2  6509  dfmpq2  6510  ordpipqqs  6529  enq0enq  6586  mulnnnq0  6605  ltsrprg  6889  axcnre  7012  axmulgt0  7149  addltmul  8217  ltxr  8795  sumsqeq0  9497  dvds2lem  10119  opoe  10206  omoe  10207  opeo  10208  omeo  10209
  Copyright terms: Public domain W3C validator