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  6530  fvopab3ig  6931  fvmptt  6955  fvn0elsuppb  8117  tfr3  8324  omordi  8487  odi  8500  nnmordi  8552  php  9123  fiint  9218  ordiso2  9408  cfcoflem  10170  zorn2lem5  10398  inar1  10673  psslinpr  10929  recexsrlem  11001  qaddcl  12865  qmulcl  12867  elfznelfzo  13675  expcan  14078  ltexp2  14079  bernneq  14138  expnbnd  14141  relexpaddg  14962  lcmfunsnlem2lem1  16551  initoeu2lem1  17923  elcls3  22999  opnneissb  23030  txbas  23483  grpoidinvlem3  30488  grporcan  30500  shscli  31299  spansncol  31550  spanunsni  31561  spansncvi  31634  homco1  31783  homulass  31784  atomli  32364  chirredlem1  32372  cdj1i  32415  satffunlem  35466  frinfm  37795  filbcmb  37800  unichnidl  38091  dmncan1  38136  pclfinclN  40069  iccelpart  47557  prmdvdsfmtnof1lem2  47709  gpgcubic  48203  gpg5nbgr3star  48205  scmsuppss  48495  iscnrm3lem4  49060