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  5550  isopolem  7291  issmo2  8281  smores  8284  inawina  10601  gchina  10610  repswcshw  14735  coprmprod  16588  issubmnd  18686  issubg2  19071  issubrng2  20491  issubrg2  20525  rnglidlmsgrp  21201  rnglidlrng  21202  ocv2ss  21628  issubassa3  21821  sslm  23243  cmetcaulem  25244  bdayfinbndlem1  28463  axcontlem4  29040  axcontlem8  29044  redwlk  29744  clwwlknwwlksn  30113  numclwwlk1lem2foa  30429  dipsubdir  30923  constrconj  33902  subgrpth  35328  cgr3tr4  36246  idinside  36278  ftc1anclem7  37900  fzmul  37942  fdc1  37947  rngosubdi  38146  rngosubdir  38147  cdlemg33a  40966  grtrimap  48194  grimgrtri  48195  grlimgrtri  48249  upwlkwlk  48385
  Copyright terms: Public domain W3C validator