MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anim123i Structured version   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  3032  eloprabga  6152  le2tri3i  9193  elfzo1  11163  unitgrp  15762  isdrngd  15850  bcthlem5  19271  rngosn  21982  chirredlem2  23884  rexdiv  24162  colinearalg  25814  axcontlem8  25875  nnssi2  26170  nnssi3  26171  welb  26392  isdrngo2  26528  expgrowthi  27482  elfzmlbm  28054  elfzmlbp  28055  elfz0fzfz0  28062  fzmmmeqm  28063  flltdivnn0lt  28089  swrdvalodmlem1  28123  swrd0swrd  28127  swrdswrd  28129  swrdccatin2  28140  swrdccat  28146  2cshw1lem1  28178  2cshw2lem2  28183  2cshw2lem3  28184  cshwssizelem2  28208  usgra2adedgwlk  28233  bnj944  29210  bnj969  29218  leatb  29991  paddasslem9  30526  paddasslem10  30527  dvhvaddass  31796
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