Theorem exp4b 379

Description: An exportation inference.

Hypothesis

Ref	Expression
exp4b.1	|- ((ph /\ ps) -> ((ch /\ th) -> ta))

Assertion

Ref	Expression
exp4b	|- (ph -> (ps -> (ch -> (th -> ta))))

Proof of Theorem exp4b

Step	Hyp	Ref	Expression
1		exp4b.1	. . 3 |- ((ph /\ ps) -> ((ch /\ th) -> ta))
2	1	exp3a 374	. 2 |- ((ph /\ ps) -> (ch -> (th -> ta)))
3	2	ex 371	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  exp43 384  reuss2 2327  wereu 2972  tz7.7 3001  fvco 3885  f1oweALT 4020  onfununi 4209  omcl 4307  oecl 4308  odi 4346  oeordi 4350  nnmcl 4370  nnecl 4371  inf3lem2 4759  genpnmax 5264  mulclprlem 5275  prlem934 5293  prlem936 5309  reclem3pr 5312  reclem4pr 5313  mulcmpblnr 5337  lemul12a 5988  nnmulcl 6086  sup2 6219  uzind 6376  zbtwnre 6393  qbtwnre 6418  expgt0 6783  expgt1 6786  le2sq2 6829  expnbnd 6852  cau4ii 7121  cau5i 7122  caubndi 7129  iserzmulc1 7339  unbenlem 7716  infpnlem1 7718  lmle 8171  ubthlem5 8791  occli 9457  projlem26 9487  projlem28 9489  spansneleq 9769  elspansn4 9772  cvmdi 10532  atcvat3i 10605  mdsymlem3 10614  icmpmon 11271  reconnlem1 11507  fmfnfmlem1 11700  fclsfneii 11740  totbndbnd 12000  heiborlem16 12026

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 145  df-an 223

Copyright terms: Public domain