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

Theorem 3anim123i 1140
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 979 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 980 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 981 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1135 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  3anim1i  1141  3anim3i  1142  syl3an  1227  syl3anl  1236  spc3egv  3046  eloprabga  6189  le2tri3i  9234  elfzo1  11204  unitgrp  15803  isdrngd  15891  bcthlem5  19312  rngosn  22023  chirredlem2  23925  rexdiv  24203  colinearalg  25880  axcontlem8  25941  nnssi2  26236  nnssi3  26237  welb  26476  isdrngo2  26612  expgrowthi  27565  uzletr  28150  elfzmlbm  28153  elfzmlbp  28154  elfz0fzfz0  28161  fzmmmeqm  28162  el2fzo  28185  flltdivnn0lt  28194  swrdvalodmlem1  28245  swrd0swrd  28255  swrdswrd  28257  swrdccatin2  28268  swrdccat  28274  2cshw1lem1  28306  2cshw2lem2  28311  2cshw2lem3  28312  cshwssizelem2  28339  usgra2adedgwlk  28378  bnj944  29407  bnj969  29415  leatb  30188  paddasslem9  30723  paddasslem10  30724  dvhvaddass  31993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator