Theorem exp43 442

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp53  453  funssres  6604  fvopab3ig  7012  fvmptt  7037  fvn0elsuppb  8226  tfr3  8435  omordi  8602  odi  8615  nnmordi  8668  php  9250  fiint  9346  ordiso2  9536  cfcoflem  10377  zorn2lem5  10605  inar1  10887  psslinpr  11143  recexsrlem  11215  qaddcl  13120  qmulcl  13122  elfznelfzo  13935  expcan  14339  ltexp2  14340  bernneq  14400  expnbnd  14403  relexpaddg  15235  lcmfunsnlem2lem1  16842  initoeu2lem1  18218  elcls3  23431  opnneissb  23462  txbas  23916  grpoidinvlem3  31138  grporcan  31150  shscli  31949  spansncol  32200  spanunsni  32211  spansncvi  32284  homco1  32433  homulass  32434  atomli  33014  chirredlem1  33022  cdj1i  33065  satffunlem  36333  frinfm  38861  filbcmb  38866  unichnidl  39157  dmncan1  39202  pclfinclN  41199  iccelpart  48720  prmdvdsfmtnof1lem2  48875  gpgcubic  49382  gpg5nbgr3star  49384  idomcanl  49649  scmsuppss  49688  iscnrm3lem4  50255