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  6961  fvn0elsuppb  8123  tfr3  8330  omordi  8493  odi  8506  nnmordi  8559  php  9131  fiint  9227  ordiso2  9420  cfcoflem  10182  zorn2lem5  10410  inar1  10686  psslinpr  10942  recexsrlem  11014  qaddcl  12878  qmulcl  12880  elfznelfzo  13689  expcan  14092  ltexp2  14093  bernneq  14152  expnbnd  14155  relexpaddg  14976  lcmfunsnlem2lem1  16565  initoeu2lem1  17938  elcls3  23027  opnneissb  23058  txbas  23511  grpoidinvlem3  30581  grporcan  30593  shscli  31392  spansncol  31643  spanunsni  31654  spansncvi  31727  homco1  31876  homulass  31877  atomli  32457  chirredlem1  32465  cdj1i  32508  satffunlem  35595  frinfm  37932  filbcmb  37937  unichnidl  38228  dmncan1  38273  pclfinclN  40206  iccelpart  47675  prmdvdsfmtnof1lem2  47827  gpgcubic  48321  gpg5nbgr3star  48323  scmsuppss  48613  iscnrm3lem4  49177