ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3anim123i Unicode version

Theorem 3anim123i 1166
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 1002 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ps )
3 3anim123i.2 . . 3  |-  ( ch 
->  th )
433ad2ant2 1003 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  th )
5 3anim123i.3 . . 3  |-  ( ta 
->  et )
653ad2ant3 1004 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  et )
72, 4, 63jca 1161 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  3anim1i  1167  3anim2i  1168  3anim3i  1169  syl3an  1258  syl3anl  1267  spc3egv  2777  spc3gv  2778  eloprabga  5858  le2tri3i  7884  fzmmmeqm  9850  elfz1b  9882  elfz0fzfz0  9915  elfzmlbp  9921  elfzo1  9979  flltdivnn0lt  10089  modmulconst  11536  nndvdslegcd  11665
  Copyright terms: Public domain W3C validator