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  6576  fvopab3ig  6981  fvmptt  7006  fvn0elsuppb  8182  tfr3  8391  omordi  8558  odi  8571  nnmordi  8624  php  9206  fiint  9302  ordiso2  9493  cfcoflem  10331  zorn2lem5  10559  inar1  10841  psslinpr  11097  recexsrlem  11169  qaddcl  13074  qmulcl  13076  elfznelfzo  13888  expcan  14292  ltexp2  14293  bernneq  14353  expnbnd  14356  relexpaddg  15186  lcmfunsnlem2lem1  16793  initoeu2lem1  18169  elcls3  23381  opnneissb  23412  txbas  23866  grpoidinvlem3  31090  grporcan  31102  shscli  31901  spansncol  32152  spanunsni  32163  spansncvi  32236  homco1  32385  homulass  32386  atomli  32966  chirredlem1  32974  cdj1i  33017  satffunlem  36135  frinfm  38637  filbcmb  38642  unichnidl  38933  dmncan1  38978  pclfinclN  40975  iccelpart  48459  prmdvdsfmtnof1lem2  48614  gpgcubic  49121  gpg5nbgr3star  49123  idomcanl  49388  scmsuppss  49427  iscnrm3lem4  49988