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

Theorem 3anim123d 1398
 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 584 . . 3 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
4 3anim123d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anim12d 584 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) → ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1033 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1033 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73imtr4g 284 1 (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  pofun  4975  isopolem  6495  issmo2  7333  smores  7336  inawina  9391  gchina  9400  repswcshw  13409  coprmprod  15213  issubmnd  17141  issubg2  17432  issubrg2  18623  ocv2ss  19836  sslm  20913  cmetcaulem  22894  axcontlem4  25647  axcontlem8  25651  redwlk  26136  3cycl3dv  26170  3v3e3cycl1  26172  constr3trllem5  26182  el2wlkonotot0  26399  dipsubdir  27087  cgr3tr4  31329  idinside  31361  ftc1anclem7  32661  fzmul  32707  fdc1  32712  rngosubdi  32914  rngosubdir  32915  cdlemg33a  35012  wlk1wlk  40846  red1wlk  40881  lidlmsgrp  41716  lidlrng  41717
 Copyright terms: Public domain W3C validator