Theorem exp43 437

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  exp53  448  funssres  6268  fvopab3ig  6631  fvmptt  6654  fvn0elsuppb  7698  tfr3  7887  omordi  8042  odi  8055  nnmordi  8107  php  8548  fiint  8641  ordiso2  8825  cfcoflem  9540  zorn2lem5  9768  inar1  10043  psslinpr  10299  recexsrlem  10371  qaddcl  12214  qmulcl  12216  elfznelfzo  12992  expcan  13383  ltexp2  13384  bernneq  13440  expnbnd  13443  relexpaddg  14246  lcmfunsnlem2lem1  15811  initoeu2lem1  17103  elcls3  21375  opnneissb  21406  txbas  21859  grpoidinvlem3  27974  grporcan  27986  shscli  28785  spansncol  29036  spanunsni  29047  spansncvi  29120  homco1  29269  homulass  29270  atomli  29850  chirredlem1  29858  cdj1i  29901  satffunlem  32257  frinfm  34561  filbcmb  34566  unichnidl  34860  dmncan1  34905  pclfinclN  36636  iccelpart  43095  prmdvdsfmtnof1lem2  43249  scmsuppss  43920