Theorem exp43 440

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp43.1	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
exp43	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem exp43

Step	Hyp	Ref	Expression
1		exp43.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
2	1	ex 416	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	exp4b 434	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  exp53  451  funssres  6402  fvopab3ig  6792  fvmptt  6816  fvn0elsuppb  7901  tfr3  8113  omordi  8272  odi  8285  nnmordi  8337  php  8808  fiint  8926  ordiso2  9109  cfcoflem  9851  zorn2lem5  10079  inar1  10354  psslinpr  10610  recexsrlem  10682  qaddcl  12526  qmulcl  12528  elfznelfzo  13312  expcan  13704  ltexp2  13705  bernneq  13761  expnbnd  13764  relexpaddg  14581  lcmfunsnlem2lem1  16158  initoeu2lem1  17474  elcls3  21934  opnneissb  21965  txbas  22418  grpoidinvlem3  28541  grporcan  28553  shscli  29352  spansncol  29603  spanunsni  29614  spansncvi  29687  homco1  29836  homulass  29837  atomli  30417  chirredlem1  30425  cdj1i  30468  satffunlem  33030  frinfm  35579  filbcmb  35584  unichnidl  35875  dmncan1  35920  pclfinclN  37650  iccelpart  44501  prmdvdsfmtnof1lem2  44653  scmsuppss  45324  iscnrm3lem4  45846