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

Theorem 3anbi123d 1275
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 464 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 464 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 949 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 949 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 222 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  3anbi12d  1276  3anbi13d  1277  3anbi23d  1278  limeq  4269  smoeq  6155  tfrlemi1  6197  tfr1onlemaccex  6213  tfrcllemaccex  6226  ereq1  6404  updjud  6935  ctssdclemr  6965  elinp  7250  sup3exmid  8683  iccshftr  9745  iccshftl  9747  iccdil  9749  icccntr  9751  fzaddel  9807  elfzomelpfzo  9976  seq3f1olemstep  10242  seq3f1olemp  10243  sumeq1  11092  summodclem2  11119  summodc  11120  zsumdc  11121  divalglemnn  11542  divalglemeunn  11545  divalglemeuneg  11547  dfgcd2  11629  ctiunct  11880  isstruct2im  11896  isstruct2r  11897  fiinopn  12098  lmfval  12288  upxp  12368
  Copyright terms: Public domain W3C validator