Theorem exp43 436

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

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  exp53  447  funssres  6462  fvopab3ig  6853  fvmptt  6877  fvn0elsuppb  7968  tfr3  8201  omordi  8359  odi  8372  nnmordi  8424  php  8897  fiint  9021  ordiso2  9204  cfcoflem  9959  zorn2lem5  10187  inar1  10462  psslinpr  10718  recexsrlem  10790  qaddcl  12634  qmulcl  12636  elfznelfzo  13420  expcan  13815  ltexp2  13816  bernneq  13872  expnbnd  13875  relexpaddg  14692  lcmfunsnlem2lem1  16271  initoeu2lem1  17645  elcls3  22142  opnneissb  22173  txbas  22626  grpoidinvlem3  28769  grporcan  28781  shscli  29580  spansncol  29831  spanunsni  29842  spansncvi  29915  homco1  30064  homulass  30065  atomli  30645  chirredlem1  30653  cdj1i  30696  satffunlem  33263  frinfm  35820  filbcmb  35825  unichnidl  36116  dmncan1  36161  pclfinclN  37891  iccelpart  44773  prmdvdsfmtnof1lem2  44925  scmsuppss  45596  iscnrm3lem4  46118