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

Theorem 3anim123i 1138
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 977 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 978 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 979 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1133 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 935
This theorem is referenced by:  3anim1i  1139  3anim3i  1140  syl3an  1225  syl3anl  1234  spc3egv  2957  eloprabga  6060  le2tri3i  9096  unitgrp  15659  isdrngd  15747  bcthlem5  18965  rngosn  21503  chirredlem2  23405  elfzo1  23675  rexdiv  23696  colinearalg  25365  axcontlem8  25426  nnssi2  25721  nnssi3  25722  welb  26009  isdrngo2  26180  expgrowthi  27141  bnj944  28722  bnj969  28730  leatb  29541  paddasslem9  30076  paddasslem10  30077  dvhvaddass  31346
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 937
  Copyright terms: Public domain W3C validator