Theorem exp43 384

Description: An exportation inference.

Hypothesis

Ref	Expression
exp43.1	⊢ (((φ ⋀ ψ) ⋀ (χ ⋀ θ)) → τ)

Assertion

Ref	Expression
exp43	⊢ (φ → (ψ → (χ → (θ → τ))))

Proof of Theorem exp43

Step	Hyp	Ref	Expression
1		exp43.1	. . 3 ⊢ (((φ ⋀ ψ) ⋀ (χ ⋀ θ)) → τ)
2	1	ex 371	. 2 ⊢ ((φ ⋀ ψ) → ((χ ⋀ θ) → τ))
3	2	exp4b 379	1 ⊢ (φ → (ψ → (χ → (θ → τ))))

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  funssres 3657  fvopab3ig 3889  fvopab2 3902  tfrlem2 4213  tfr3 4227  omordi 4333  odi 4346  oaabs 4392  eceqopreq 4454  xpdom2 4583  mapenlem2 4637  php 4660  fiint 4703  zorn2lem5 4938  unxpdomlem 4993  psslinpr 5289  prlem936b 5308  recexsrlem 5366  qaddcl 6408  qmulcl 6410  seqzrn 6752  exprec 6789  exprecOLD 6790  bernneq 6849  bernneqOLD 6850  expnbnd 6852  fsumcom 7231  climmulc2 7332  xpnnen 7711  infxpidmlem11 7774  tgss2 7849  subtop 7858  elcls3 7921  opnneissb 7938  metge0 8029  rnblssm 8061  blss 8063  metcnp 8098  iscau3 8149  iscau4 8151  metcnp4 8181  xplmi 8184  bcthlem33 8242  grpidinvlem3 8263  grprcan 8280  grplcan 8292  nvcnpi3 8676  nvcnpi4 8677  minvecex 8838  spwmo 8918  shscli 9557  spansncol 9767  spanunsni 9778  spansncvi 9875  homco1 10007  homulass 10008  atomli 10591  irredlem1 10599  cdj1i 10642  neifil 11080  cmpmon 11270  exp53 11353  elfiun 11421  finsschain 11425  ordiso 11426  ordtypelem7 11433  hscptsscld 11491  cncomp 11494  comptoppr 11495  cnconn 11503  conntoppr 11504  fnemeet1 11589  fnemeet2 11590  filssufillem 11655  ufilen 11664  fmfnfmlem4 11703  fcluscnplem 11729  filnetlem5 11767  frinfm 11850  filbcmb 11857

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 145  df-an 223

Copyright terms: Public domain