Theorem exp43 436

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 412	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	exp4b 430	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  exp53  447  funssres  6536  fvopab3ig  6937  fvmptt  6962  fvn0elsuppb  8124  tfr3  8331  omordi  8494  odi  8507  nnmordi  8560  php  9134  fiint  9230  ordiso2  9423  cfcoflem  10185  zorn2lem5  10413  inar1  10689  psslinpr  10945  recexsrlem  11017  qaddcl  12906  qmulcl  12908  elfznelfzo  13719  expcan  14122  ltexp2  14123  bernneq  14182  expnbnd  14185  relexpaddg  15006  lcmfunsnlem2lem1  16598  initoeu2lem1  17972  elcls3  23058  opnneissb  23089  txbas  23542  grpoidinvlem3  30592  grporcan  30604  shscli  31403  spansncol  31654  spanunsni  31665  spansncvi  31738  homco1  31887  homulass  31888  atomli  32468  chirredlem1  32476  cdj1i  32519  satffunlem  35599  frinfm  38070  filbcmb  38075  unichnidl  38366  dmncan1  38411  pclfinclN  40410  iccelpart  47905  prmdvdsfmtnof1lem2  48060  gpgcubic  48567  gpg5nbgr3star  48569  scmsuppss  48859  iscnrm3lem4  49423