Theorem exp43 301

Description: An exportation inference.

Hypothesis

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

Assertion

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

<ðR ALIGN=LEFT>

Proof of Theorem exp43

Step	Hyp	Ref	Expression
1		exp43.1	. . 3 ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ)
2	1	exp 291	. 2 ⊢ ((φ ∧ ψ) → ((χ ∧ θ) → τ))
3	2	exp4b 296	1 ⊢ (φ → (ψ → (χ → (θ → τ))))

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  funssres 2698  fvopab3ig 2869  fvopab2 2878  tfrlem2 2950  tfr3 2964  omordi 3164  eceqopreq 3249  xpdom2 3345  mapenlem2 3385  php 3409  fiint 3445  zornlem5 3607  unxpdomlem 3649  psslinpr 3929  prlem936b 3948  recexsrlem 4006  qaddclt 4642  qmulclt 4644  xpnnen 4927  infxpidmlem11 4943  spansncol 5473  spanunsn 5482  spansncv 5542

This theorem was proved from Gxioms:  ax-1 3  ax-2 4  ax-3 ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org