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  6542  fvopab3ig  6943  fvmptt  6968  fvn0elsuppb  8131  tfr3  8338  omordi  8501  odi  8514  nnmordi  8567  php  9141  fiint  9237  ordiso2  9430  cfcoflem  10194  zorn2lem5  10422  inar1  10698  psslinpr  10954  recexsrlem  11026  qaddcl  12915  qmulcl  12917  elfznelfzo  13728  expcan  14131  ltexp2  14132  bernneq  14191  expnbnd  14194  relexpaddg  15015  lcmfunsnlem2lem1  16607  initoeu2lem1  17981  elcls3  23048  opnneissb  23079  txbas  23532  grpoidinvlem3  30577  grporcan  30589  shscli  31388  spansncol  31639  spanunsni  31650  spansncvi  31723  homco1  31872  homulass  31873  atomli  32453  chirredlem1  32461  cdj1i  32504  satffunlem  35583  frinfm  38056  filbcmb  38061  unichnidl  38352  dmncan1  38397  pclfinclN  40396  iccelpart  47893  prmdvdsfmtnof1lem2  48048  gpgcubic  48555  gpg5nbgr3star  48557  scmsuppss  48847  iscnrm3lem4  49411