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

Theorem 3anim123i 1181
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 1017 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 1018 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 1019 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1176 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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
This theorem is referenced by:  3anim1i  1182  3anim2i  1183  3anim3i  1184  syl3an  1270  syl3anl  1279  spc3egv  3202  eloprabga  6373  le2tri3i  9714  fzmmmeqm  11717  elfz1b  11748  elfz0fzfz0  11777  elfzmlbm  11782  elfzmlbp  11783  elfzo0z  11833  elfzo1  11839  ssfzoulel  11874  flltdivnn0lt  11933  swrdspsleq  12636  swrdswrd  12648  swrdccatin2  12675  swrdccat  12681  mulmoddvds  13903  symg2hash  16227  pmtrdifellem2  16308  unitgrp  17117  isdrngd  17221  mdetunilem9  18917  bcthlem5  21530  colinearalg  23917  axcontlem8  23978  usgra2adedgwlk  24318  rngosn  25110  chirredlem2  27014  rexdiv  27318  nnssi2  29525  nnssi3  29526  welb  29858  isdrngo2  29992  expgrowthi  30866  el2fzo  31834  lincvalpr  32118  bnj944  33093  bnj969  33101  leatb  34107  paddasslem9  34642  paddasslem10  34643  dvhvaddass  35912
  Copyright terms: Public domain W3C validator