Theorem exp43 439

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exp53  450  funssres  6398  fvopab3ig  6764  fvmptt  6788  fvn0elsuppb  7847  tfr3  8035  omordi  8192  odi  8205  nnmordi  8257  php  8701  fiint  8795  ordiso2  8979  cfcoflem  9694  zorn2lem5  9922  inar1  10197  psslinpr  10453  recexsrlem  10525  qaddcl  12365  qmulcl  12367  elfznelfzo  13143  expcan  13534  ltexp2  13535  bernneq  13591  expnbnd  13594  relexpaddg  14412  lcmfunsnlem2lem1  15982  initoeu2lem1  17274  elcls3  21691  opnneissb  21722  txbas  22175  grpoidinvlem3  28283  grporcan  28295  shscli  29094  spansncol  29345  spanunsni  29356  spansncvi  29429  homco1  29578  homulass  29579  atomli  30159  chirredlem1  30167  cdj1i  30210  satffunlem  32648  frinfm  35025  filbcmb  35030  unichnidl  35324  dmncan1  35369  pclfinclN  37101  iccelpart  43613  prmdvdsfmtnof1lem2  43767  scmsuppss  44440