Theorem exp43 393

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 380	. 2 |- ((ph /\ ps) -> ((ch /\ th) -> ta))
3	2	exp4b 388	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  funssres 3609  fvopab3ig 3835  fvopab2 3848  tfrlem2 3970  tfr3 3984  omordi 4255  odi 4268  oaabs 4310  eceqopreq 4374  xpdom2 4505  mapenlem2 4555  php 4578  fiint 4620  zorn2lem5 4854  unxpdomlem 4908  psslinpr 5200  prlem936b 5219  recexsrlem 5277  qaddcl 6321  qmulcl 6323  seqzrn 6646  recexp 6684  bernneq 6741  expnbnd 6743  fsumcom 7118  climmulc2 7219  xpnnen 7591  infxpidmlem11 7654  tgss2 7726  subtop 7733  elcls3 7796  opnneissb 7813  metge0 7904  rnblssm 7936  blss 7938  metcnp 7972  iscau3 8023  iscau4 8025  metcnp4 8055  xplmi 8058  bcthlem33 8116  grpidinvlem3 8135  grprcan 8147  grplcan 8159  nvcnpi3 8506  nvcnpi4 8507  minvecex 8662  spwmo 8740  shscli 9364  spansncol 9574  spanunsni 9585  spansncvi 9680  homco1 9810  homulass 9811  atomli 10393  irredlem1 10401  cdj1i 10444  neifil 10661  cmpmon 10825

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 154  df-an 232

Copyright terms: Public domain