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  6563  fvopab3ig  6967  fvmptt  6991  fvn0elsuppb  8163  tfr3  8370  omordi  8533  odi  8546  nnmordi  8598  php  9177  fiint  9284  fiintOLD  9285  ordiso2  9475  cfcoflem  10232  zorn2lem5  10460  inar1  10735  psslinpr  10991  recexsrlem  11063  qaddcl  12931  qmulcl  12933  elfznelfzo  13740  expcan  14141  ltexp2  14142  bernneq  14201  expnbnd  14204  relexpaddg  15026  lcmfunsnlem2lem1  16615  initoeu2lem1  17983  elcls3  22977  opnneissb  23008  txbas  23461  grpoidinvlem3  30442  grporcan  30454  shscli  31253  spansncol  31504  spanunsni  31515  spansncvi  31588  homco1  31737  homulass  31738  atomli  32318  chirredlem1  32326  cdj1i  32369  satffunlem  35395  frinfm  37736  filbcmb  37741  unichnidl  38032  dmncan1  38077  pclfinclN  39951  iccelpart  47438  prmdvdsfmtnof1lem2  47590  gpgcubic  48074  gpg5nbgr3star  48076  scmsuppss  48363  iscnrm3lem4  48928