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

Theorem 3anim123i 1181
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 1017 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 1018 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 1019 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1176 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 975
This theorem is referenced by:  3anim1i  1182  3anim2i  1183  3anim3i  1184  syl3an  1270  syl3anl  1279  spc3egv  3198  eloprabga  6388  le2tri3i  9731  fzmmmeqm  11742  elfz1b  11773  elfz0fzfz0  11804  elfzmlbmOLD  11810  elfzmlbp  11811  elfzo1  11869  ssfzoulel  11908  flltdivnn0lt  11967  swrdswrd  12696  swrdccatin2  12723  swrdccat  12729  mulmoddvds  14055  symg2hash  16548  pmtrdifellem2  16628  unitgrp  17442  isdrngd  17547  bcthlem5  21892  colinearalg  24339  axcontlem8  24400  usgra2adedgwlk  24740  rngosn  25532  chirredlem2  27436  rexdiv  27774  nnssi2  30082  nnssi3  30083  isdrngo2  30523  expgrowthi  31400  el2fzo  32561  2zrngasgrp  32848  2zrngmsgrp  32855  lincvalpr  33121  bnj944  34097  bnj969  34105  leatb  35118  paddasslem9  35653  paddasslem10  35654  dvhvaddass  36925
  Copyright terms: Public domain W3C validator