NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  bi2anan9 GIF version

Theorem bi2anan9 843
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 685 . 2 (φ → ((ψ τ) ↔ (χ τ)))
3 bi2an9.2 . . 3 (θ → (τη))
43anbi2d 684 . 2 (θ → ((χ τ) ↔ (χ η)))
52, 4sylan9bb 680 1 ((φ θ) → ((ψ τ) ↔ (χ η)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  bi2anan9r  844  2mo  2282  2eu6  2289  2reu5  3044  ralprg  3775  raltpg  3777  prssg  3862  ssofeq  4077  ncfinraise  4481  ncfinlower  4483  nnpweq  4523  opelopab2a  4702  brsi  4761  dfxp2  5113  fvopab4t  5385  dff13  5471  resoprab2  5582  ovig  5597  brtxp  5783  fnpprod  5843  fundmen  6043  endisj  6051  mucnc  6131  peano4nc  6150  ce0addcnnul  6179  ce0nnulb  6182  ceclb  6183  ceclr  6187  sbth  6206  dflec2  6210  letc  6231  addcdi  6250  fnfrec  6320
  Copyright terms: Public domain W3C validator