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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  exp43 384  reuss2 2275  wereu 2945  tz7.7 2973  fvco 3774  f1oweALT 3906  omcl 4171  oecl 4172  odi 4210  oeordi 4214  nnmcl 4230  nnecl 4231  inf3lem2 4614  genpnmax 5110  mulclprlem 5121  prlem934 5139  prlem936 5155  reclem3pr 5158  reclem4pr 5159  mulcmpblnr 5183  lemul12it 5844  nnmulclt 5941  sup2 6051  uzind 6205  zbtwnre 6221  qbtwnre 6278  expgt0t 6589  expgt1t 6592  le2sqit 6632  expnbndt 6654  cau4i 6918  cau5 6919  caubnd 6926  iserzmulc1 7136  unbenlem 7504  infpnlem1 7506  lmle 7960  ubthlem5 8533  occl 9181  projlem26 9211  projlem28 9213  spansneleq 9493  elspansn4t 9496  cvmd 10251  atcvat3 10323  mdsymlem3 10332  icmpmon 10744

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