Theorem exp43 637

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

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  exp53  644  funssres  5830  fvopab3ig  6173  fvmptt  6193  fvn0elsuppb  7176  tfr3  7359  omordi  7510  odi  7523  nnmordi  7575  php  8006  fiint  8099  ordiso2  8280  cfcoflem  8954  zorn2lem5  9182  inar1  9453  psslinpr  9709  recexsrlem  9780  qaddcl  11636  qmulcl  11638  elfznelfzo  12394  expcan  12730  ltexp2  12731  bernneq  12807  expnbnd  12810  relexpaddg  13587  lcmfunsnlem2lem1  15135  initoeu2lem1  16433  elcls3  20639  opnneissb  20670  txbas  21122  grpoidinvlem3  26510  grporcan  26522  shscli  27366  spansncol  27617  spanunsni  27628  spansncvi  27701  homco1  27850  homulass  27851  atomli  28431  chirredlem1  28439  cdj1i  28482  frinfm  32503  filbcmb  32508  unichnidl  32803  dmncan1  32848  pclfinclN  34057  iccelpart  39776  prmdvdsfmtnof1lem2  39840  scmsuppss  41949