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

This theorem is referenced by:  exp53  447  funssres  6612  fvopab3ig  7012  fvmptt  7036  fvn0elsuppb  8205  tfr3  8438  omordi  8603  odi  8616  nnmordi  8668  php  9245  phpOLD  9257  fiint  9364  fiintOLD  9365  ordiso2  9553  cfcoflem  10310  zorn2lem5  10538  inar1  10813  psslinpr  11069  recexsrlem  11141  qaddcl  13005  qmulcl  13007  elfznelfzo  13808  expcan  14206  ltexp2  14207  bernneq  14265  expnbnd  14268  relexpaddg  15089  lcmfunsnlem2lem1  16672  initoeu2lem1  18068  elcls3  23107  opnneissb  23138  txbas  23591  grpoidinvlem3  30535  grporcan  30547  shscli  31346  spansncol  31597  spanunsni  31608  spansncvi  31681  homco1  31830  homulass  31831  atomli  32411  chirredlem1  32419  cdj1i  32462  satffunlem  35386  frinfm  37722  filbcmb  37727  unichnidl  38018  dmncan1  38063  pclfinclN  39933  iccelpart  47358  prmdvdsfmtnof1lem2  47510  gpgcubic  47970  gpg5nbgr3star  47972  scmsuppss  48216  iscnrm3lem4  48733