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

Theorem 3anbi123d 1206
Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
Hypotheses
Ref Expression
bi3d.1 (φ → (ψχ))
bi3d.2 (φ → (θτ))
bi3d.3 (φ → (ηζ))
Assertion
Ref Expression
3anbi123d (φ → ((ψ θ η) ↔ (χ τ ζ)))

Proof of Theorem 3anbi123d
StepHypRef Expression
1 bi3d.1 . . . 4 (φ → (ψχ))
2 bi3d.2 . . . 4 (φ → (θτ))
31, 2anbi12d 442 . . 3 (φ → ((ψ θ) ↔ (χ τ)))
4 bi3d.3 . . 3 (φ → (ηζ))
53, 4anbi12d 442 . 2 (φ → (((ψ θ) η) ↔ ((χ τ) ζ)))
6 df-3an 886 . 2 ((ψ θ η) ↔ ((ψ θ) η))
7 df-3an 886 . 2 ((χ τ ζ) ↔ ((χ τ) ζ))
85, 6, 73bitr4g 212 1 (φ → ((ψ θ η) ↔ (χ τ ζ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 884
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  df-3an 886
This theorem is referenced by:  3anbi12d  1207  3anbi13d  1208  3anbi23d  1209  sbc3ang  2814  limeq  4080  smoeq  5846  tfrlemi1  5887  ereq1  6049  elinp  6456  iccshftr  8592  iccshftl  8594  iccdil  8596  icccntr  8598  fzaddel  8652  elfzomelpfzo  8817
  Copyright terms: Public domain W3C validator