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  6525  fvopab3ig  6925  fvmptt  6949  fvn0elsuppb  8111  tfr3  8318  omordi  8481  odi  8494  nnmordi  8546  php  9116  fiint  9211  ordiso2  9401  cfcoflem  10160  zorn2lem5  10388  inar1  10663  psslinpr  10919  recexsrlem  10991  qaddcl  12860  qmulcl  12862  elfznelfzo  13670  expcan  14073  ltexp2  14074  bernneq  14133  expnbnd  14136  relexpaddg  14957  lcmfunsnlem2lem1  16546  initoeu2lem1  17918  elcls3  22996  opnneissb  23027  txbas  23480  grpoidinvlem3  30481  grporcan  30493  shscli  31292  spansncol  31543  spanunsni  31554  spansncvi  31627  homco1  31776  homulass  31777  atomli  32357  chirredlem1  32365  cdj1i  32408  satffunlem  35433  frinfm  37774  filbcmb  37779  unichnidl  38070  dmncan1  38115  pclfinclN  39988  iccelpart  47463  prmdvdsfmtnof1lem2  47615  gpgcubic  48109  gpg5nbgr3star  48111  scmsuppss  48401  iscnrm3lem4  48966