HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem imp41 368
Description: An importation inference.
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 350 . 2 |- ((ph /\ ps) -> (ch -> (th -> ta)))
32imp31 362 1 |- ((((ph /\ ps) /\ ch) /\ th) -> ta)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  adantlll 396  adantllr 397  peano5 3143  oelim 4153  prlem936b 5126  lemul12it 5800  uzwo4OLD 6158  uzwo 6387  uzwoOLD 6388  cau3ir 6852  caucvglem4 7096  fsum0diag4 7196  infxpidmlem11 7505  iscncl 7709  xplmi 7907  cmsss 7931  bcthlem28 7960  grprcan 7997  grpinveu 7998  blocnilem 8395  projlem28 9129  osumlem4 9498  spansncv 9514  sumdmdi 10249  cmpmon 10585
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain