Theorem exp43 384

Description: An exportation inference.

Hypothesis

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

Assertion

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

Proof of Theorem exp43

Step	Hyp	Ref	Expression
1		exp43.1	. . 3 |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
2	1	ex 373	. 2 |- ((ph /\ ps) -> ((ch /\ th) -> ta))
3	2	exp4b 379	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  funssres 3548  fvopab3ig 3773  fvopab2 3786  tfrlem2 3907  tfr3 3921  omordi 4190  odi 4203  oaabs 4245  eceqopreq 4306  xpdom2 4431  mapenlem2 4479  php 4502  fiint 4543  zorn2lem5 4775  unxpdomlem 4826  psslinpr 5118  prlem936b 5137  recexsrlem 5195  qaddclt 6219  qmulclt 6221  seqzrn 6502  recexpt 6540  bernneq 6597  expnbndt 6599  fsumcom 6981  climmulc2 7082  xpnnen 7458  infxpidmlem11 7522  tgss2t 7597  subtop 7606  elcls3 7671  opnneissb 7688  metge0 7781  bl2in 7805  rnblssm 7813  blss 7815  metcnp 7849  iscau3 7900  iscau4 7902  metcnp4 7932  xplmi 7935  bcthlem33 7993  grpidinvlem3 8012  grprcan 8025  grplcan 8037  nvcnpi4 8383  minvecex 8537  spwmo 8613  shscl 9236  spansncol 9447  spanunsn 9459  spansncv 9554  homco1t 9684  homulasst 9685  atoml 10265  irredlem1 10273  cdj1 10316  neifil 10501  cmpmon 10657

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