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

Theorem 3anim123d 1445
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 609 . . 3 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
4 3anim123d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anim12d 609 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) → ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1089 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1089 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73imtr4g 296 1 (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  pofun  5610  isopolem  7365  issmo2  8389  smores  8392  inawina  10730  gchina  10739  repswcshw  14850  coprmprod  16698  issubmnd  18774  issubg2  19159  issubrng2  20558  issubrg2  20592  rnglidlmsgrp  21256  rnglidlrng  21257  ocv2ss  21691  issubassa3  21886  sslm  23307  cmetcaulem  25322  axcontlem4  28982  axcontlem8  28986  redwlk  29690  clwwlknwwlksn  30057  numclwwlk1lem2foa  30373  dipsubdir  30867  constrconj  33786  subgrpth  35139  cgr3tr4  36053  idinside  36085  ftc1anclem7  37706  fzmul  37748  fdc1  37753  rngosubdi  37952  rngosubdir  37953  cdlemg33a  40708  grtrimap  47915  grimgrtri  47916  grlimgrtri  47963  upwlkwlk  48055
  Copyright terms: Public domain W3C validator