Theorem exp43 440

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  exp53  451  funssres  6561  fvopab3ig  6967  fvmptt  6992  fvn0elsuppb  8156  tfr3  8365  omordi  8530  odi  8543  nnmordi  8596  php  9171  fiint  9267  ordiso2  9460  cfcoflem  10226  zorn2lem5  10454  inar1  10730  psslinpr  10986  recexsrlem  11058  qaddcl  12963  qmulcl  12965  elfznelfzo  13776  expcan  14179  ltexp2  14180  bernneq  14239  expnbnd  14242  relexpaddg  15063  lcmfunsnlem2lem1  16655  initoeu2lem1  18030  elcls3  23123  opnneissb  23154  txbas  23607  grpoidinvlem3  30655  grporcan  30667  shscli  31466  spansncol  31717  spanunsni  31728  spansncvi  31801  homco1  31950  homulass  31951  atomli  32531  chirredlem1  32539  cdj1i  32582  satffunlem  35715  frinfm  38198  filbcmb  38203  unichnidl  38494  dmncan1  38539  pclfinclN  40538  iccelpart  48003  prmdvdsfmtnof1lem2  48158  gpgcubic  48665  gpg5nbgr3star  48667  scmsuppss  48957  iscnrm3lem4  49521