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

Theorem 3anim123d 1443
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 295 1 (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 206  df-an 397  df-3an 1089
This theorem is referenced by:  pofun  5606  isopolem  7344  issmo2  8351  smores  8354  inawina  10687  gchina  10696  repswcshw  14764  coprmprod  16600  issubmnd  18654  issubg2  19023  issubrg2  20343  ocv2ss  21232  issubassa3  21426  sslm  22810  cmetcaulem  24812  axcontlem4  28263  axcontlem8  28267  redwlk  28967  clwwlknwwlksn  29329  numclwwlk1lem2foa  29645  dipsubdir  30139  subgrpth  34194  cgr3tr4  35093  idinside  35125  ftc1anclem7  36653  fzmul  36695  fdc1  36700  rngosubdi  36899  rngosubdir  36900  cdlemg33a  39663  upwlkwlk  46596  issubrng2  46816  rnglidlmsgrp  46836  rnglidlrng  46837
  Copyright terms: Public domain W3C validator