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

Theorem 3anim123d 1281
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 550 . . 3
4 3anim123d.3 . . 3
53, 4anim12d 550 . 2
6 df-3an 952 . 2
7 df-3an 952 . 2
85, 6, 73imtr4g 264 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  /\w3a 950
This theorem is referenced by:  pofun  4628  isopolem  6004  issmo2  6769  smores  6772  inawina  8803  gchina  8812  repswcshw  12387  issubmnd  15389  issubg2  15633  issubrg2  16698  ocv2ss  17806  sslm  18607  cmetcaulem  20499  axcontlem4  22892  axcontlem8  22896  redwlk  23184  3cycl3dv  23207  3v3e3cycl1  23209  constr3trllem5  23219  grponnncan2  23420  dipsubdir  23927  cgr3tr4  27785  idinside  27817  ftc1anclem7  28144  fzmul  28307  fdc1  28313  rngosubdi  28430  rngosubdir  28431  el2wlkonotot0  30065  cdlemg33a  33787
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 179  df-an 364  df-3an 952
  Copyright terms: Public domain W3C validator