Theorem exp43 641

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  exp53  648  funssres  6091  fvopab3ig  6440  fvmptt  6462  fvn0elsuppb  7480  tfr3  7664  omordi  7815  odi  7828  nnmordi  7880  php  8309  fiint  8402  ordiso2  8585  cfcoflem  9286  zorn2lem5  9514  inar1  9789  psslinpr  10045  recexsrlem  10116  qaddcl  11997  qmulcl  11999  elfznelfzo  12767  expcan  13107  ltexp2  13108  bernneq  13184  expnbnd  13187  relexpaddg  13992  lcmfunsnlem2lem1  15553  initoeu2lem1  16865  elcls3  21089  opnneissb  21120  txbas  21572  grpoidinvlem3  27669  grporcan  27681  shscli  28485  spansncol  28736  spanunsni  28747  spansncvi  28820  homco1  28969  homulass  28970  atomli  29550  chirredlem1  29558  cdj1i  29601  frinfm  33843  filbcmb  33848  unichnidl  34143  dmncan1  34188  pclfinclN  35739  iccelpart  41879  prmdvdsfmtnof1lem2  42007  scmsuppss  42663