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

This theorem is referenced by:  exp53  448  funssres  6478  fvopab3ig  6871  fvmptt  6895  fvn0elsuppb  7997  tfr3  8230  omordi  8397  odi  8410  nnmordi  8462  php  8993  phpOLD  9005  fiint  9091  ordiso2  9274  cfcoflem  10028  zorn2lem5  10256  inar1  10531  psslinpr  10787  recexsrlem  10859  qaddcl  12705  qmulcl  12707  elfznelfzo  13492  expcan  13887  ltexp2  13888  bernneq  13944  expnbnd  13947  relexpaddg  14764  lcmfunsnlem2lem1  16343  initoeu2lem1  17729  elcls3  22234  opnneissb  22265  txbas  22718  grpoidinvlem3  28868  grporcan  28880  shscli  29679  spansncol  29930  spanunsni  29941  spansncvi  30014  homco1  30163  homulass  30164  atomli  30744  chirredlem1  30752  cdj1i  30795  satffunlem  33363  frinfm  35893  filbcmb  35898  unichnidl  36189  dmncan1  36234  pclfinclN  37964  iccelpart  44885  prmdvdsfmtnof1lem2  45037  scmsuppss  45708  iscnrm3lem4  46230