MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anim123d Structured version   Visualization version   GIF version

Theorem 3anim123d 1444
Description: Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)
Hypotheses
Ref Expression
3anim123d.1 (𝜑 → (𝜓𝜒))
3anim123d.2 (𝜑 → (𝜃𝜏))
3anim123d.3 (𝜑 → (𝜂𝜁))
Assertion
Ref Expression
3anim123d (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))

Proof of Theorem 3anim123d
StepHypRef Expression
1 3anim123d.1 . . . 4 (𝜑 → (𝜓𝜒))
2 3anim123d.2 . . . 4 (𝜑 → (𝜃𝜏))
31, 2anim12d 610 . . 3 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
4 3anim123d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anim12d 610 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) → ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1090 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1090 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73imtr4g 296 1 (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090
This theorem is referenced by:  pofun  5607  isopolem  7342  issmo2  8349  smores  8352  inawina  10685  gchina  10694  repswcshw  14762  coprmprod  16598  issubmnd  18652  issubg2  19021  issubrg2  20339  ocv2ss  21226  issubassa3  21420  sslm  22803  cmetcaulem  24805  axcontlem4  28225  axcontlem8  28229  redwlk  28929  clwwlknwwlksn  29291  numclwwlk1lem2foa  29607  dipsubdir  30101  subgrpth  34125  cgr3tr4  35024  idinside  35056  ftc1anclem7  36567  fzmul  36609  fdc1  36614  rngosubdi  36813  rngosubdir  36814  cdlemg33a  39577  upwlkwlk  46517  issubrng2  46737  rnglidlmsgrp  46757  rnglidlrng  46758
  Copyright terms: Public domain W3C validator