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

Theorem 3anbi123d 1273
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 462 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 462 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 947 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 947 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 222 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 945
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 947
This theorem is referenced by:  3anbi12d  1274  3anbi13d  1275  3anbi23d  1276  limeq  4267  smoeq  6153  tfrlemi1  6195  tfr1onlemaccex  6211  tfrcllemaccex  6224  ereq1  6402  updjud  6933  ctssdclemr  6963  elinp  7246  sup3exmid  8672  iccshftr  9717  iccshftl  9719  iccdil  9721  icccntr  9723  fzaddel  9779  elfzomelpfzo  9948  seq3f1olemstep  10214  seq3f1olemp  10215  sumeq1  11064  summodclem2  11091  summodc  11092  zsumdc  11093  divalglemnn  11511  divalglemeunn  11514  divalglemeuneg  11516  dfgcd2  11598  ctiunct  11848  isstruct2im  11864  isstruct2r  11865  fiinopn  12066  lmfval  12256  upxp  12336
  Copyright terms: Public domain W3C validator