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

Theorem 3anim123i 1190
Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
Hypotheses
Ref Expression
3anim123i.1  |-  ( ph  ->  ps )
3anim123i.2  |-  ( ch 
->  th )
3anim123i.3  |-  ( ta 
->  et )
Assertion
Ref Expression
3anim123i  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )

Proof of Theorem 3anim123i
StepHypRef Expression
1 3anim123i.1 . . 3  |-  ( ph  ->  ps )
213ad2ant1 1026 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 1027 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 1028 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1185 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  3anim1i  1191  3anim2i  1192  3anim3i  1193  syl3an  1306  syl3anl  1315  spc3egv  3176  eloprabga  6397  le2tri3i  9763  fzmmmeqm  11830  elfz1b  11862  elfz0fzfz0  11893  elfzmlbmOLD  11899  elfzmlbp  11900  elfzo1  11962  ssfzoulel  12002  flltdivnn0lt  12062  swrdswrd  12801  swrdccatin2  12828  swrdccat  12834  mulmoddvds  14341  nndvdslegcd  14453  ncoprmlnprm  14648  symg2hash  16989  pmtrdifellem2  17069  unitgrp  17830  isdrngd  17935  bcthlem5  22189  colinearalg  24786  axcontlem8  24847  usgra2adedgwlk  25187  rngosn  25977  chirredlem2  27879  rexdiv  28233  bnj944  29537  bnj969  29545  nnssi2  30900  nnssi3  30901  isdrngo2  31901  leatb  32567  paddasslem9  33102  paddasslem10  33103  dvhvaddass  34374  expgrowthi  36319  nnsum4primesodd  38281  nnsum4primesoddALTV  38282  2zrngasgrp  38698  2zrngmsgrp  38705  lincvalpr  38971  refdivmptf  39114  refdivmptfv  39118
  Copyright terms: Public domain W3C validator