Theorem exp43 442

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp53  453  funssres  6584  fvopab3ig  6989  fvmptt  7014  fvn0elsuppb  8201  tfr3  8410  omordi  8577  odi  8590  nnmordi  8643  php  9225  fiint  9321  ordiso2  9512  cfcoflem  10353  zorn2lem5  10581  inar1  10863  psslinpr  11119  recexsrlem  11191  qaddcl  13096  qmulcl  13098  elfznelfzo  13911  expcan  14315  ltexp2  14316  bernneq  14376  expnbnd  14379  relexpaddg  15211  lcmfunsnlem2lem1  16818  initoeu2lem1  18194  elcls3  23406  opnneissb  23437  txbas  23891  grpoidinvlem3  31113  grporcan  31125  shscli  31924  spansncol  32175  spanunsni  32186  spansncvi  32259  homco1  32408  homulass  32409  atomli  32989  chirredlem1  32997  cdj1i  33040  satffunlem  36252  frinfm  38762  filbcmb  38767  unichnidl  39058  dmncan1  39103  pclfinclN  41100  iccelpart  48608  prmdvdsfmtnof1lem2  48763  gpgcubic  49270  gpg5nbgr3star  49272  idomcanl  49537  scmsuppss  49576  iscnrm3lem4  50143