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

Theorem bi2anan9 606
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 465 . 2 (𝜑 → ((𝜓𝜏) ↔ (𝜒𝜏)))
3 bi2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43anbi2d 464 . 2 (𝜃 → ((𝜒𝜏) ↔ (𝜒𝜂)))
52, 4sylan9bb 462 1 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  bi2anan9r  607  rspc2gv  2868  ralprg  3658  raltpg  3660  prssg  3764  prsspwg  3767  opelopab2a  4283  opelxp  4674  eqrel  4733  eqrelrel  4745  brcog  4812  dff13  5790  resoprab2  5993  ovig  6018  dfoprab4f  6218  f1o2ndf1  6253  eroveu  6652  th3qlem1  6663  th3qlem2  6664  th3q  6666  oviec  6667  endisj  6850  exmidapne  7289  dfplpq2  7383  dfmpq2  7384  ordpipqqs  7403  enq0enq  7460  mulnnnq0  7479  ltsrprg  7776  axcnre  7910  axmulgt0  8059  addltmul  9185  ltxr  9805  sumsqeq0  10630  mul0inf  11281  dvds2lem  11842  opoe  11932  omoe  11933  opeo  11934  omeo  11935  gcddvds  11996  dfgcd2  12047  pcqmul  12335  xpsfrnel2  12822  eqgval  13162  txbasval  14227  cnmpt12  14247  cnmpt22  14254  2sqlem7  14929
  Copyright terms: Public domain W3C validator