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  6581  fvopab3ig  6986  fvmptt  7011  fvn0elsuppb  8183  tfr3  8392  omordi  8557  odi  8570  nnmordi  8623  php  9205  fiint  9300  ordiso2  9491  cfcoflem  10278  zorn2lem5  10506  inar1  10788  psslinpr  11044  recexsrlem  11116  qaddcl  13019  qmulcl  13021  elfznelfzo  13833  expcan  14237  ltexp2  14238  bernneq  14297  expnbnd  14300  relexpaddg  15130  lcmfunsnlem2lem1  16734  initoeu2lem1  18109  elcls3  23314  opnneissb  23345  txbas  23799  grpoidinvlem3  30995  grporcan  31007  shscli  31806  spansncol  32057  spanunsni  32068  spansncvi  32141  homco1  32290  homulass  32291  atomli  32871  chirredlem1  32879  cdj1i  32922  satffunlem  35988  frinfm  38493  filbcmb  38498  unichnidl  38789  dmncan1  38834  pclfinclN  40831  iccelpart  48341  prmdvdsfmtnof1lem2  48496  gpgcubic  49003  gpg5nbgr3star  49005  idomcanl  49270  scmsuppss  49309  iscnrm3lem4  49870