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

Theorem 3anim123d 1442
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  5614  isopolem  7364  issmo2  8387  smores  8390  inawina  10727  gchina  10736  repswcshw  14846  coprmprod  16694  issubmnd  18786  issubg2  19171  issubrng2  20574  issubrg2  20608  rnglidlmsgrp  21273  rnglidlrng  21274  ocv2ss  21708  issubassa3  21903  sslm  23322  cmetcaulem  25335  axcontlem4  28996  axcontlem8  29000  redwlk  29704  clwwlknwwlksn  30066  numclwwlk1lem2foa  30382  dipsubdir  30876  constrconj  33749  subgrpth  35118  cgr3tr4  36033  idinside  36065  ftc1anclem7  37685  fzmul  37727  fdc1  37732  rngosubdi  37931  rngosubdir  37932  cdlemg33a  40688  grtrimap  47850  grimgrtri  47851  grlimgrtri  47898  upwlkwlk  47982
  Copyright terms: Public domain W3C validator