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

Theorem imp41 577
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
imp41  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )

Proof of Theorem imp41
StepHypRef Expression
1 imp4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21imp 419 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  ( th  ->  ta ) ) )
32imp31 422 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  3anassrs  1175  peano5  4827  oelim  6737  lemul12a  9824  uzwo  10495  uzwoOLD  10496  elfznelfzo  11147  injresinj  11155  catidd  13860  grpinveu  14794  2ndcctbss  17471  grpoinveu  21763  spansncvi  23107  sumdmdii  23871  unichnidl  26531  hbtlem2  27196  swrdswrd  28011  el2spthonot  28067  2pthfrgra  28115  frgrancvvdeqlemB  28141  2spotiundisj  28165  usg2spot2nb  28168  ad4ant13  28252  ad4ant14  28253  ad4ant123  28254  ad4ant124  28255  ad4ant134  28256  ad4ant23  28257  ad4ant24  28258  ad4ant234  28259  ad5ant13  28261  ad5ant14  28262  ad5ant15  28263  ad5ant23  28264  ad5ant24  28265  ad5ant25  28266  ad5ant245  28267  ad5ant234  28268  ad5ant235  28269  ad5ant123  28270  ad5ant124  28271  ad5ant125  28272  ad5ant134  28273  ad5ant135  28274  ad5ant145  28275  ad5ant1345  28276  ad5ant2345  28277  linepsubN  30234  pmapsub  30250  cdlemkid4  31416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator