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

Theorem 3anim123i 1139
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 978 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 979 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 980 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1134 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  3anim1i  1140  3anim3i  1141  syl3an  1226  syl3anl  1235  spc3egv  3000  eloprabga  6119  le2tri3i  9159  elfzo1  11128  unitgrp  15727  isdrngd  15815  bcthlem5  19234  rngosn  21945  chirredlem2  23847  rexdiv  24125  colinearalg  25753  axcontlem8  25814  nnssi2  26109  nnssi3  26110  welb  26328  isdrngo2  26464  expgrowthi  27418  elfzmlbm  27977  elfzmlbp  27978  swrd0swrd  28009  swrdswrd  28011  swrdccatin2  28018  swrdccatin12lem3  28024  usgra2adedgwlk  28046  bnj944  29015  bnj969  29023  leatb  29775  paddasslem9  30310  paddasslem10  30311  dvhvaddass  31580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator