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  6610  fvopab3ig  7012  fvmptt  7036  fvn0elsuppb  8206  tfr3  8439  omordi  8604  odi  8617  nnmordi  8669  php  9247  phpOLD  9259  fiint  9366  fiintOLD  9367  ordiso2  9555  cfcoflem  10312  zorn2lem5  10540  inar1  10815  psslinpr  11071  recexsrlem  11143  qaddcl  13007  qmulcl  13009  elfznelfzo  13811  expcan  14209  ltexp2  14210  bernneq  14268  expnbnd  14271  relexpaddg  15092  lcmfunsnlem2lem1  16675  initoeu2lem1  18059  elcls3  23091  opnneissb  23122  txbas  23575  grpoidinvlem3  30525  grporcan  30537  shscli  31336  spansncol  31587  spanunsni  31598  spansncvi  31671  homco1  31820  homulass  31821  atomli  32401  chirredlem1  32409  cdj1i  32452  satffunlem  35406  frinfm  37742  filbcmb  37747  unichnidl  38038  dmncan1  38083  pclfinclN  39952  iccelpart  47420  prmdvdsfmtnof1lem2  47572  gpgcubic  48035  gpg5nbgr3star  48037  scmsuppss  48287  iscnrm3lem4  48833