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

Theorem bi2anan9 571
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 453 . 2 (𝜑 → ((𝜓𝜏) ↔ (𝜒𝜏)))
3 bi2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43anbi2d 452 . 2 (𝜃 → ((𝜒𝜏) ↔ (𝜒𝜂)))
52, 4sylan9bb 450 1 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bi2anan9r  572  rspc2gv  2725  ralprg  3476  raltpg  3478  prssg  3577  prsspwg  3579  opelopab2a  4066  opelxp  4440  eqrel  4495  eqrelrel  4507  brcog  4571  dff13  5508  resoprab2  5699  ovig  5723  dfoprab4f  5920  f1o2ndf1  5950  eroveu  6335  th3qlem1  6346  th3qlem2  6347  th3q  6349  oviec  6350  endisj  6492  dfplpq2  6857  dfmpq2  6858  ordpipqqs  6877  enq0enq  6934  mulnnnq0  6953  ltsrprg  7237  axcnre  7360  axmulgt0  7502  addltmul  8585  ltxr  9178  sumsqeq0  9931  dvds2lem  10683  opoe  10770  omoe  10771  opeo  10772  omeo  10773  gcddvds  10830  dfgcd2  10878
  Copyright terms: Public domain W3C validator