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

Theorem 3anim123i 1173
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 1009 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 1010 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 1011 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1168 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  3anim1i  1174  3anim3i  1175  syl3an  1260  syl3anl  1269  spc3egv  3061  eloprabga  6177  le2tri3i  9504  uzletr  10869  elfz0fzfz0  11485  elfzmlbm  11490  elfzmlbp  11491  fzmmmeqm  11492  elfz1b  11527  elfzo0z  11589  elfzo1  11595  ssfzoulel  11621  flltdivnn0lt  11677  swrdspsleq  12342  swrdswrd  12354  swrdccatin2  12378  swrdccat  12384  symg2hash  15902  pmtrdifellem2  15983  unitgrp  16759  isdrngd  16857  mdetunilem9  18426  bcthlem5  20839  colinearalg  23156  axcontlem8  23217  rngosn  23891  chirredlem2  25795  rexdiv  26101  nnssi2  28301  nnssi3  28302  welb  28630  isdrngo2  28764  expgrowthi  29607  uzuzle  30190  el2fzo  30212  mulmoddvds  30246  usgra2adedgwlk  30306  lincvalpr  30952  bnj944  31931  bnj969  31939  leatb  32937  paddasslem9  33472  paddasslem10  33473  dvhvaddass  34742
  Copyright terms: Public domain W3C validator