Theorem exp4b 410

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 405	. 2 |- ((ph /\ ps) -> (ch -> (th -> ta)))
3	2	ex 402	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  exp43 415  reuss2 2870  wereu 3654  tz7.7 3684  fvco 4736  f1oweALT 4883  onfununi 5116  omclOLD 5217  oeclOLD 5219  odi 5258  oeordi 5262  nnmclOLD 5284  nneclOLD 5286  inf3lem2 5720  genpnmax 6262  mulclprlem 6273  prlem934 6291  prlem936 6307  reclem3pr 6310  reclem4pr 6311  mulcmpblnr 6335  lemul12a 7026  nnmulcl 7124  sup2 7260  uzind 7417  zbtwnre 7434  qbtwnre 7459  expgt0 7831  expgt1 7834  le2sq2 7877  expnbnd 7901  cau4ii 8170  cau5i 8171  caubndi 8178  iserzmulc1 8396  unbenlem 8773  infpnlem1 8775  lmle 9238  ubthlem5 9876  occli 10814  projlem26 10844  projlem28 10846  spansneleq 11126  elspansn4 11129  cvmdi 11896  atcvat3i 11968  mdsymlem3 11977  dfon2lem8 13856  soseq 13955  axdenselem5 14023  icmpmon 15165  reconnlem1 15446  fmfnfmlem1 15594  fclsfneii 15628  fzmul 15790  totbndbnd 15944  heiborlem16 15970  hlrelat2 17052  cvrat3 17075  pointpsub 17231  pmaple 17241

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 164  df-an 242

Copyright terms: Public domain