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 3443  fundmen 4428  fiint 4559  fiintOLD 4560  ltexprlem6 5147  prlem936b 5154  divne0t 5729  divgt0t 5855  divge0t 5856  le2sqit 6632  bcclt 6972  clmi1 7086  climmulc2 7129  isummulc1ALT 7213  infxpidmlem11 7562  basis2t 7615  neindisj 7731  lmcvgnns 7943  cmsss 7997  bcthlem1 7999  bcthlem20 8018  spwmo 8656  spansneleq 9493  elspansn4t 9496  cnopct 9837  cnfnct 9854  adjmult 10025  kbass6t 10054  mdsl0 10237  irredlem1 10317

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