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

Theorem 3anbi123d 1291
 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 465 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 465 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 965 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 965 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 222 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 963 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 965 This theorem is referenced by:  3anbi12d  1292  3anbi13d  1293  3anbi23d  1294  limeq  4332  smoeq  6227  tfrlemi1  6269  tfr1onlemaccex  6285  tfrcllemaccex  6298  ereq1  6476  updjud  7012  ctssdclemr  7042  elinp  7373  sup3exmid  8807  iccshftr  9876  iccshftl  9878  iccdil  9880  icccntr  9882  fzaddel  9939  elfzomelpfzo  10108  seq3f1olemstep  10378  seq3f1olemp  10379  sumeq1  11229  summodclem2  11256  summodc  11257  zsumdc  11258  prodmodclem2  11451  prodmodc  11452  divalglemnn  11782  divalglemeunn  11785  divalglemeuneg  11787  dfgcd2  11870  ctiunct  12128  isstruct2im  12147  isstruct2r  12148  fiinopn  12349  lmfval  12539  upxp  12619  2irrexpqap  13242  dceqnconst  13579  dcapnconst  13580
 Copyright terms: Public domain W3C validator