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  6587  fvopab3ig  6992  fvmptt  7017  fvn0elsuppb  8186  tfr3  8395  omordi  8560  odi  8573  nnmordi  8626  php  9201  fiint  9296  ordiso2  9487  cfcoflem  10274  zorn2lem5  10502  inar1  10778  psslinpr  11034  recexsrlem  11106  qaddcl  13007  qmulcl  13009  elfznelfzo  13821  expcan  14225  ltexp2  14226  bernneq  14285  expnbnd  14288  relexpaddg  15116  lcmfunsnlem2lem1  16721  initoeu2lem1  18096  elcls3  23277  opnneissb  23308  txbas  23761  grpoidinvlem3  30895  grporcan  30907  shscli  31706  spansncol  31957  spanunsni  31968  spansncvi  32041  homco1  32190  homulass  32191  atomli  32771  chirredlem1  32779  cdj1i  32822  satffunlem  35914  frinfm  38427  filbcmb  38432  unichnidl  38723  dmncan1  38768  pclfinclN  40765  iccelpart  48223  prmdvdsfmtnof1lem2  48378  gpgcubic  48885  gpg5nbgr3star  48887  idomcanl  49153  scmsuppss  49192  iscnrm3lem4  49755