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

Theorem 3anim123d 1306
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 563 . . 3
4 3anim123d.3 . . 3
53, 4anim12d 563 . 2
6 df-3an 975 . 2
7 df-3an 975 . 2
85, 6, 73imtr4g 270 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  pofun  4821  isopolem  6241  issmo2  7039  smores  7042  inawina  9089  gchina  9098  repswcshw  12780  issubmnd  15948  issubg2  16216  issubrg2  17449  ocv2ss  18704  sslm  19800  cmetcaulem  21727  axcontlem4  24270  axcontlem8  24274  redwlk  24608  3cycl3dv  24642  3v3e3cycl1  24644  constr3trllem5  24654  el2wlkonotot0  24872  grponnncan2  25256  dipsubdir  25763  cgr3tr4  29702  idinside  29734  ftc1anclem7  30096  fzmul  30233  fdc1  30239  rngosubdi  30356  rngosubdir  30357  lidlmsgrp  32732  lidlrng  32733  cdlemg33a  36432
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator