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

Theorem imbi12i 316
 Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12i.1 (φψ)
imbi12i.2 (χθ)
Assertion
Ref Expression
imbi12i ((φχ) ↔ (ψθ))

Proof of Theorem imbi12i
StepHypRef Expression
1 imbi12i.2 . . 3 (χθ)
21imbi2i 303 . 2 ((φχ) ↔ (φθ))
3 imbi12i.1 . . 3 (φψ)
43imbi1i 315 . 2 ((φθ) ↔ (ψθ))
52, 4bitri 240 1 ((φχ) ↔ (ψθ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 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 This theorem is referenced by:  orimdi  820  rb-bijust  1514  nfbii  1569  sb8mo  2223  cbvmo  2241  raleqbii  2644  rmo5  2827  cbvrmo  2834  ss2ab  3334  sscon34  3661  evenodddisjlem1  4515  tfinnn  4534  cotr  5026  cnvsym  5027  intasym  5028  intirr  5029  dffun2  5119  funcnvuni  5161  fvfullfunlem1  5861  clos1induct  5880
 Copyright terms: Public domain W3C validator