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

Theorem 3anim123i 1137
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 976 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 977 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 978 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1132 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  3anim1i  1138  3anim3i  1139  syl3an  1224  syl3anl  1233  spc3egv  2872  eloprabga  5934  le2tri3i  8949  unitgrp  15449  isdrngd  15537  bcthlem5  18750  rngosn  21071  chirredlem2  22971  rexdiv  23109  elfzo1  23279  colinearalg  24538  axcontlem8  24599  nnssi2  24894  nnssi3  24895  elo  25041  oriso  25214  cmptdst2  25571  welb  26417  isdrngo2  26589  expgrowthi  27550  bnj944  28970  bnj969  28978  leatb  29482  paddasslem9  30017  paddasslem10  30018  dvhvaddass  31287
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator