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  6534  fvopab3ig  6935  fvmptt  6960  fvn0elsuppb  8122  tfr3  8329  omordi  8492  odi  8505  nnmordi  8558  php  9132  fiint  9228  ordiso2  9421  cfcoflem  10183  zorn2lem5  10411  inar1  10687  psslinpr  10943  recexsrlem  11015  qaddcl  12904  qmulcl  12906  elfznelfzo  13717  expcan  14120  ltexp2  14121  bernneq  14180  expnbnd  14183  relexpaddg  15004  lcmfunsnlem2lem1  16596  initoeu2lem1  17970  elcls3  23056  opnneissb  23087  txbas  23540  grpoidinvlem3  30590  grporcan  30602  shscli  31401  spansncol  31652  spanunsni  31663  spansncvi  31736  homco1  31885  homulass  31886  atomli  32466  chirredlem1  32474  cdj1i  32517  satffunlem  35597  frinfm  38060  filbcmb  38065  unichnidl  38356  dmncan1  38401  pclfinclN  40400  iccelpart  47895  prmdvdsfmtnof1lem2  48050  gpgcubic  48557  gpg5nbgr3star  48559  scmsuppss  48849  iscnrm3lem4  49413