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

Theorem bi2anan9 538
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 438 . 2 (𝜑 → ((𝜓𝜏) ↔ (𝜒𝜏)))
3 bi2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43anbi2d 437 . 2 (𝜃 → ((𝜒𝜏) ↔ (𝜒𝜂)))
52, 4sylan9bb 435 1 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bi2anan9r  539  ralprg  3418  raltpg  3420  prssg  3518  prsspwg  3520  opelopab2a  3999  opelxp  4352  eqrel  4407  eqrelrel  4419  brcog  4480  dff13  5385  resoprab2  5576  ovig  5600  dfoprab4f  5797  f1o2ndf1  5827  eroveu  6175  th3qlem1  6186  th3qlem2  6187  th3q  6189  oviec  6190  endisj  6276  dfplpq2  6424  dfmpq2  6425  ordpipqqs  6444  enq0enq  6501  mulnnnq0  6520  ltsrprg  6804  axcnre  6927  axmulgt0  7062  addltmul  8125  ltxr  8653  sumsqeq0  9201
  Copyright terms: Public domain W3C validator