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  6622  fvopab3ig  7025  fvmptt  7049  fvn0elsuppb  8222  tfr3  8455  omordi  8622  odi  8635  nnmordi  8687  php  9273  phpOLD  9285  fiint  9394  fiintOLD  9395  ordiso2  9584  cfcoflem  10341  zorn2lem5  10569  inar1  10844  psslinpr  11100  recexsrlem  11172  qaddcl  13030  qmulcl  13032  elfznelfzo  13822  expcan  14219  ltexp2  14220  bernneq  14278  expnbnd  14281  relexpaddg  15102  lcmfunsnlem2lem1  16685  initoeu2lem1  18081  elcls3  23112  opnneissb  23143  txbas  23596  grpoidinvlem3  30538  grporcan  30550  shscli  31349  spansncol  31600  spanunsni  31611  spansncvi  31684  homco1  31833  homulass  31834  atomli  32414  chirredlem1  32422  cdj1i  32465  satffunlem  35369  frinfm  37695  filbcmb  37700  unichnidl  37991  dmncan1  38036  pclfinclN  39907  iccelpart  47307  prmdvdsfmtnof1lem2  47459  scmsuppss  48097  iscnrm3lem4  48616