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

Theorem bi2anan9 526
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 441 . 2 (φ → ((ψ τ) ↔ (χ τ)))
3 bi2an9.2 . . 3 (θ → (τη))
43anbi2d 440 . 2 (θ → ((χ τ) ↔ (χ η)))
52, 4sylan9bb 438 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  527  ralprg  3391  raltpg  3393  prssg  3491  prsspwg  3493  opelopab2a  3972  opelxp  4297  eqrel  4352  eqrelrel  4364  brcog  4425  dff13  5328  resoprab2  5517  ovig  5541  dfoprab4f  5738  f1o2ndf1  5768  eroveu  6104  th3qlem1  6115  th3qlem2  6116  th3q  6118  oviec  6119  dfplpq2  6207  dfmpq2  6208  ordpipqqs  6227  enq0enq  6280  mulnnnq0  6299  ltsrprg  6491  axcnre  6574  axmulgt0  6693
  Copyright terms: Public domain W3C validator