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  3008  eloprabga  6127  le2tri3i  9167  elfzo1  11136  unitgrp  15735  isdrngd  15823  bcthlem5  19242  rngosn  21953  chirredlem2  23855  rexdiv  24133  colinearalg  25761  axcontlem8  25822  nnssi2  26117  nnssi3  26118  welb  26336  isdrngo2  26472  expgrowthi  27426  elfzmlbm  27985  elfzmlbp  27986  swrd0swrd  28017  swrdswrd  28019  swrdccatin2  28026  swrdccatin12lem3  28032  usgra2adedgwlk  28054  bnj944  29027  bnj969  29035  leatb  29787  paddasslem9  30322  paddasslem10  30323  dvhvaddass  31592
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