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  6580  fvopab3ig  6982  fvmptt  7006  fvn0elsuppb  8180  tfr3  8413  omordi  8578  odi  8591  nnmordi  8643  php  9221  phpOLD  9231  fiint  9338  fiintOLD  9339  ordiso2  9529  cfcoflem  10286  zorn2lem5  10514  inar1  10789  psslinpr  11045  recexsrlem  11117  qaddcl  12981  qmulcl  12983  elfznelfzo  13788  expcan  14187  ltexp2  14188  bernneq  14247  expnbnd  14250  relexpaddg  15072  lcmfunsnlem2lem1  16657  initoeu2lem1  18027  elcls3  23021  opnneissb  23052  txbas  23505  grpoidinvlem3  30487  grporcan  30499  shscli  31298  spansncol  31549  spanunsni  31560  spansncvi  31633  homco1  31782  homulass  31783  atomli  32363  chirredlem1  32371  cdj1i  32414  satffunlem  35423  frinfm  37759  filbcmb  37764  unichnidl  38055  dmncan1  38100  pclfinclN  39969  iccelpart  47447  prmdvdsfmtnof1lem2  47599  gpgcubic  48081  gpg5nbgr3star  48083  scmsuppss  48346  iscnrm3lem4  48910