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

Theorem imp41 578
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 420 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  ( th  ->  ta ) ) )
32imp31 423 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  3anassrs  1176  peano5  4870  oelim  6780  lemul12a  9870  uzwo  10541  uzwoOLD  10542  elfznelfzo  11194  injresinj  11202  catidd  13907  grpinveu  14841  2ndcctbss  17520  grpoinveu  21812  spansncvi  23156  sumdmdii  23920  unichnidl  26643  hbtlem2  27307  swrdswrd  28221  2cshw1lem2  28271  el2spthonot  28390  2pthfrgra  28463  frgrancvvdeqlemB  28489  2spotiundisj  28513  usg2spot2nb  28516  ad4ant13  28600  ad4ant14  28601  ad4ant123  28602  ad4ant124  28603  ad4ant134  28604  ad4ant23  28605  ad4ant24  28606  ad4ant234  28607  ad5ant13  28609  ad5ant14  28610  ad5ant15  28611  ad5ant23  28612  ad5ant24  28613  ad5ant25  28614  ad5ant245  28615  ad5ant234  28616  ad5ant235  28617  ad5ant123  28618  ad5ant124  28619  ad5ant125  28620  ad5ant134  28621  ad5ant135  28622  ad5ant145  28623  ad5ant1345  28624  ad5ant2345  28625  linepsubN  30611  pmapsub  30627  cdlemkid4  31793
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 179  df-an 362
  Copyright terms: Public domain W3C validator