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

Theorem 3anbi123d 1312
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 473 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 473 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 980 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 980 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 223 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  3anbi12d  1313  3anbi13d  1314  3anbi23d  1315  limeq  4377  smoeq  6290  tfrlemi1  6332  tfr1onlemaccex  6348  tfrcllemaccex  6361  ereq1  6541  updjud  7080  ctssdclemr  7110  tapeq1  7250  tapeq2  7251  elinp  7472  sup3exmid  8913  iccshftr  9993  iccshftl  9995  iccdil  9997  icccntr  9999  fzaddel  10058  elfzomelpfzo  10230  seq3f1olemstep  10500  seq3f1olemp  10501  sumeq1  11362  summodclem2  11389  summodc  11390  zsumdc  11391  prodmodclem2  11584  prodmodc  11585  divalglemnn  11922  divalglemeunn  11925  divalglemeuneg  11927  dfgcd2  12014  pythagtriplem18  12280  pythagtriplem19  12281  ctiunct  12440  ssomct  12445  isstruct2im  12471  isstruct2r  12472  ptex  12712  isringd  13218  issubrg3  13373  fiinopn  13440  lmfval  13628  upxp  13708  2irrexpqap  14332  dceqnconst  14743  dcapnconst  14744
  Copyright terms: Public domain W3C validator