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

Theorem 3anim123d 1440
 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 611 . . 3 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
4 3anim123d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anim12d 611 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) → ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1086 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1086 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73imtr4g 299 1 (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  pofun  5455  isopolem  7077  issmo2  7971  smores  7974  inawina  10103  gchina  10112  repswcshw  14167  coprmprod  15997  issubmnd  17932  issubg2  18289  issubrg2  19551  ocv2ss  20366  issubassa3  20558  sslm  21911  cmetcaulem  23899  axcontlem4  26768  axcontlem8  26772  redwlk  27469  clwwlknwwlksn  27830  numclwwlk1lem2foa  28146  dipsubdir  28638  subgrpth  32506  cgr3tr4  33638  idinside  33670  ftc1anclem7  35152  fzmul  35195  fdc1  35200  rngosubdi  35399  rngosubdir  35400  cdlemg33a  38018  upwlkwlk  44382  lidlmsgrp  44565  lidlrng  44566
 Copyright terms: Public domain W3C validator