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  6560  fvopab3ig  6964  fvmptt  6988  fvn0elsuppb  8160  tfr3  8367  omordi  8530  odi  8543  nnmordi  8595  php  9171  fiint  9277  fiintOLD  9278  ordiso2  9468  cfcoflem  10225  zorn2lem5  10453  inar1  10728  psslinpr  10984  recexsrlem  11056  qaddcl  12924  qmulcl  12926  elfznelfzo  13733  expcan  14134  ltexp2  14135  bernneq  14194  expnbnd  14197  relexpaddg  15019  lcmfunsnlem2lem1  16608  initoeu2lem1  17976  elcls3  22970  opnneissb  23001  txbas  23454  grpoidinvlem3  30435  grporcan  30447  shscli  31246  spansncol  31497  spanunsni  31508  spansncvi  31581  homco1  31730  homulass  31731  atomli  32311  chirredlem1  32319  cdj1i  32362  satffunlem  35388  frinfm  37729  filbcmb  37734  unichnidl  38025  dmncan1  38070  pclfinclN  39944  iccelpart  47434  prmdvdsfmtnof1lem2  47586  gpgcubic  48070  gpg5nbgr3star  48072  scmsuppss  48359  iscnrm3lem4  48924