Theorem exp43 638

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 630	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 196  df-an 385

This theorem is referenced by:  exp53  645  funssres  5844  fvopab3ig  6188  fvmptt  6208  fvn0elsuppb  7199  tfr3  7382  omordi  7533  odi  7546  nnmordi  7598  php  8029  fiint  8122  ordiso2  8303  cfcoflem  8977  zorn2lem5  9205  inar1  9476  psslinpr  9732  recexsrlem  9803  qaddcl  11680  qmulcl  11682  elfznelfzo  12439  expcan  12775  ltexp2  12776  bernneq  12852  expnbnd  12855  relexpaddg  13641  lcmfunsnlem2lem1  15189  initoeu2lem1  16487  elcls3  20697  opnneissb  20728  txbas  21180  grpoidinvlem3  26744  grporcan  26756  shscli  27560  spansncol  27811  spanunsni  27822  spansncvi  27895  homco1  28044  homulass  28045  atomli  28625  chirredlem1  28633  cdj1i  28676  frinfm  32700  filbcmb  32705  unichnidl  33000  dmncan1  33045  pclfinclN  34254  iccelpart  39971  prmdvdsfmtnof1lem2  40035  scmsuppss  41947