Theorem exp43 441

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  exp53  452  funssres  6582  fvopab3ig  6987  fvmptt  7012  fvn0elsuppb  8178  tfr3  8387  omordi  8552  odi  8565  nnmordi  8618  php  9192  fiint  9287  ordiso2  9478  cfcoflem  10257  zorn2lem5  10485  inar1  10761  psslinpr  11017  recexsrlem  11089  qaddcl  12990  qmulcl  12992  elfznelfzo  13804  expcan  14207  ltexp2  14208  bernneq  14267  expnbnd  14270  relexpaddg  15092  lcmfunsnlem2lem1  16697  initoeu2lem1  18072  elcls3  23221  opnneissb  23252  txbas  23705  grpoidinvlem3  30836  grporcan  30848  shscli  31647  spansncol  31898  spanunsni  31909  spansncvi  31982  homco1  32131  homulass  32132  atomli  32712  chirredlem1  32720  cdj1i  32763  satffunlem  35871  frinfm  38364  filbcmb  38369  unichnidl  38660  dmncan1  38705  pclfinclN  40702  iccelpart  48159  prmdvdsfmtnof1lem2  48314  gpgcubic  48821  gpg5nbgr3star  48823  idomcanl  49089  scmsuppss  49128  iscnrm3lem4  49691