Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  bi2anan9 Structured version   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  3412  raltpg  3414  prssg  3512  prsspwg  3514  opelopab2a  3993  opelxp  4317  eqrel  4372  eqrelrel  4384  brcog  4445  dff13  5350  resoprab2  5540  ovig  5564  dfoprab4f  5761  f1o2ndf1  5791  eroveu  6133  th3qlem1  6144  th3qlem2  6145  th3q  6147  oviec  6148  endisj  6234  dfplpq2  6338  dfmpq2  6339  ordpipqqs  6358  enq0enq  6413  mulnnnq0  6432  ltsrprg  6655  axcnre  6745  axmulgt0  6868  addltmul  7918  ltxr  8445  sumsqeq0  8965
 Copyright terms: Public domain W3C validator