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

Theorem 3anim123i 1168
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 1004 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 1005 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 1006 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1163 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 960
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 185  df-an 371  df-3an 962
This theorem is referenced by:  3anim1i  1169  3anim3i  1170  syl3an  1255  syl3anl  1264  spc3egv  3058  eloprabga  6176  le2tri3i  9500  uzletr  10865  elfz0fzfz0  11481  elfzmlbm  11486  elfzmlbp  11487  fzmmmeqm  11488  elfz1b  11523  elfzo0z  11585  elfzo1  11591  ssfzoulel  11617  flltdivnn0lt  11673  swrdspsleq  12338  swrdswrd  12350  swrdccatin2  12374  swrdccat  12380  symg2hash  15895  pmtrdifellem2  15976  unitgrp  16749  isdrngd  16837  mdetunilem9  18326  bcthlem5  20739  colinearalg  23075  axcontlem8  23136  rngosn  23810  chirredlem2  25714  rexdiv  26018  nnssi2  28215  nnssi3  28216  welb  28539  isdrngo2  28673  expgrowthi  29516  uzuzle  30099  el2fzo  30121  mulmoddvds  30155  usgra2adedgwlk  30215  lincvalpr  30776  bnj944  31748  bnj969  31756  leatb  32625  paddasslem9  33160  paddasslem10  33161  dvhvaddass  34430
  Copyright terms: Public domain W3C validator