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

Theorem 3anim123d 1435
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 608 . . 3 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
4 3anim123d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anim12d 608 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) → ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1082 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1082 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73imtr4g 297 1 (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080
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 208  df-an 397  df-3an 1082
This theorem is referenced by:  pofun  5386  isopolem  6968  issmo2  7845  smores  7848  inawina  9965  gchina  9974  repswcshw  14014  coprmprod  15838  issubmnd  17761  issubg2  18052  issubrg2  19249  ocv2ss  20503  sslm  21595  cmetcaulem  23578  axcontlem4  26440  axcontlem8  26444  redwlk  27140  clwwlknwwlksn  27502  clwwlknonwwlknonb  27571  numclwwlk1lem2foa  27821  dipsubdir  28312  subgrpth  31991  cgr3tr4  33124  idinside  33156  ftc1anclem7  34525  fzmul  34569  fdc1  34574  rngosubdi  34776  rngosubdir  34777  cdlemg33a  37394  upwlkwlk  43518  lidlmsgrp  43697  lidlrng  43698
  Copyright terms: Public domain W3C validator