Theorem exp43 439

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 415	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	exp4b 433	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exp53  450  funssres  6400  fvopab3ig  6766  fvmptt  6790  fvn0elsuppb  7849  tfr3  8037  omordi  8194  odi  8207  nnmordi  8259  php  8703  fiint  8797  ordiso2  8981  cfcoflem  9696  zorn2lem5  9924  inar1  10199  psslinpr  10455  recexsrlem  10527  qaddcl  12367  qmulcl  12369  elfznelfzo  13145  expcan  13536  ltexp2  13537  bernneq  13593  expnbnd  13596  relexpaddg  14414  lcmfunsnlem2lem1  15984  initoeu2lem1  17276  elcls3  21693  opnneissb  21724  txbas  22177  grpoidinvlem3  28285  grporcan  28297  shscli  29096  spansncol  29347  spanunsni  29358  spansncvi  29431  homco1  29580  homulass  29581  atomli  30161  chirredlem1  30169  cdj1i  30212  satffunlem  32650  frinfm  35012  filbcmb  35017  unichnidl  35311  dmncan1  35356  pclfinclN  37088  iccelpart  43600  prmdvdsfmtnof1lem2  43754  scmsuppss  44427