Theorem exp43 437

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 413	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	exp4b 431	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  exp53  448  funssres  6536  fvopab3ig  6938  fvmptt  6963  fvn0elsuppb  8128  tfr3  8335  omordi  8498  odi  8511  nnmordi  8564  php  9138  fiint  9234  ordiso2  9427  cfcoflem  10192  zorn2lem5  10420  inar1  10696  psslinpr  10952  recexsrlem  11024  qaddcl  12913  qmulcl  12915  elfznelfzo  13726  expcan  14129  ltexp2  14130  bernneq  14189  expnbnd  14192  relexpaddg  15013  lcmfunsnlem2lem1  16605  initoeu2lem1  17979  elcls3  23073  opnneissb  23104  txbas  23557  grpoidinvlem3  30602  grporcan  30614  shscli  31413  spansncol  31664  spanunsni  31675  spansncvi  31748  homco1  31897  homulass  31898  atomli  32478  chirredlem1  32486  cdj1i  32529  satffunlem  35636  frinfm  38109  filbcmb  38114  unichnidl  38405  dmncan1  38450  pclfinclN  40449  iccelpart  47915  prmdvdsfmtnof1lem2  48070  gpgcubic  48577  gpg5nbgr3star  48579  scmsuppss  48869  iscnrm3lem4  49433