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 3538  fvopab3ig 3763  fvopab2 3776  tfrlem2 3897  tfr3 3911  omordi 4181  odi 4194  oaabs 4236  eceqopreq 4297  xpdom2 4422  mapenlem2 4470  php 4493  fiint 4534  zorn2lem5 4764  unxpdomlem 4815  psslinpr 5107  prlem936b 5126  recexsrlem 5184  qaddclt 6207  qmulclt 6209  seqzrn 6489  recexpt 6526  bernneq 6583  expnbndt 6585  fsumcom 6966  climmulc2 7065  xpnnen 7441  infxpidmlem11 7505  tgss2t 7579  subtop 7588  elcls3 7652  opnneissb 7669  metge0 7760  bl2in 7783  rnblssm 7791  blss 7793  metcnp 7826  iscau3 7876  metcnp4 7904  xplmi 7907  bcthlem33 7965  grpidinvlem3 7984  grprcan 7997  grplcan 8010  nvcnpi4 8355  minvecex 8509  spwmo 8580  shscl 9196  spansncol 9407  spanunsn 9419  spansncv 9514  homco1t 9644  homulasst 9645  atoml 10217  irredlem1 10225  cdj1 10265  neifil 10442  cmpmon 10585

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