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  6544  fvopab3ig  6945  fvmptt  6970  fvn0elsuppb  8133  tfr3  8340  omordi  8503  odi  8516  nnmordi  8569  php  9143  fiint  9239  ordiso2  9432  cfcoflem  10194  zorn2lem5  10422  inar1  10698  psslinpr  10954  recexsrlem  11026  qaddcl  12890  qmulcl  12892  elfznelfzo  13701  expcan  14104  ltexp2  14105  bernneq  14164  expnbnd  14167  relexpaddg  14988  lcmfunsnlem2lem1  16577  initoeu2lem1  17950  elcls3  23039  opnneissb  23070  txbas  23523  grpoidinvlem3  30593  grporcan  30605  shscli  31404  spansncol  31655  spanunsni  31666  spansncvi  31739  homco1  31888  homulass  31889  atomli  32469  chirredlem1  32477  cdj1i  32520  satffunlem  35614  frinfm  37980  filbcmb  37985  unichnidl  38276  dmncan1  38321  pclfinclN  40320  iccelpart  47787  prmdvdsfmtnof1lem2  47939  gpgcubic  48433  gpg5nbgr3star  48435  scmsuppss  48725  iscnrm3lem4  49289