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 1088 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1088 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73imtr4g 296 1 (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 1088
This theorem is referenced by:  pofun  5545  isopolem  7285  issmo2  8275  smores  8278  inawina  10587  gchina  10596  repswcshw  14725  coprmprod  16578  issubmnd  18675  issubg2  19060  issubrng2  20479  issubrg2  20513  rnglidlmsgrp  21189  rnglidlrng  21190  ocv2ss  21616  issubassa3  21809  sslm  23220  cmetcaulem  25221  axcontlem4  28952  axcontlem8  28956  redwlk  29656  clwwlknwwlksn  30025  numclwwlk1lem2foa  30341  dipsubdir  30835  constrconj  33765  subgrpth  35185  cgr3tr4  36103  idinside  36135  ftc1anclem7  37745  fzmul  37787  fdc1  37792  rngosubdi  37991  rngosubdir  37992  cdlemg33a  40811  grtrimap  48053  grimgrtri  48054  grlimgrtri  48108  upwlkwlk  48244
  Copyright terms: Public domain W3C validator