Theorem imp43 370

Description: An importation inference.

Hypothesis

Ref	Expression
imp4.1	|- (ph -> (ps -> (ch -> (th -> ta))))

Assertion

Ref	Expression
imp43	|- (((ph /\ ps) /\ (ch /\ th)) -> ta)

Proof of Theorem imp43

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	imp4b 365	. 2 |- ((ph /\ ps) -> ((ch /\ th) -> ta))
3	2	imp 350	1 |- (((ph /\ ps) /\ (ch /\ th)) -> ta)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sotri 3440  fundmen 4422  fiint 4547  ltexprlem6 5134  prlem936b 5141  divne0t 5706  divgt0t 5823  divge0t 5824  le2sqit 6582  bcclt 6940  clmi1 7054  climmulc2 7098  isummulc1ALT 7184  infxpidmlem11 7541  basis2t 7594  neindisj 7710  lmcvgnns 7926  cmsss 7980  bcthlem1 7982  bcthlem20 8001  spwmo 8637  spansneleq 9482  spansneleqOLD 9483  elspansn4t 9486  cnopct 9828  cnfnct 9845  adjmult 10016  kbass6t 10045  mdsl0 10228  irredlem1 10308

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