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

Theorem 3anbi123d 1218
 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 450 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 450 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 898 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 898 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 216 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∧ w3a 896 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114  df-3an 898 This theorem is referenced by:  3anbi12d  1219  3anbi13d  1220  3anbi23d  1221  limeq  4142  smoeq  5936  tfrlemi1  5977  ereq1  6144  elinp  6630  iccshftr  8963  iccshftl  8965  iccdil  8967  icccntr  8969  fzaddel  9024  elfzomelpfzo  9189  divalglemnn  10230  divalglemeunn  10233  divalglemeuneg  10235
 Copyright terms: Public domain W3C validator