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  6569  fvopab3ig  6975  fvmptt  7000  fvn0elsuppb  8165  tfr3  8374  omordi  8539  odi  8552  nnmordi  8605  php  9179  fiint  9274  ordiso2  9465  cfcoflem  10244  zorn2lem5  10472  inar1  10748  psslinpr  11004  recexsrlem  11076  qaddcl  12980  qmulcl  12982  elfznelfzo  13793  expcan  14196  ltexp2  14197  bernneq  14256  expnbnd  14259  relexpaddg  15080  lcmfunsnlem2lem1  16686  initoeu2lem1  18061  elcls3  23201  opnneissb  23232  txbas  23685  grpoidinvlem3  30767  grporcan  30779  shscli  31578  spansncol  31829  spanunsni  31840  spansncvi  31913  homco1  32062  homulass  32063  atomli  32643  chirredlem1  32651  cdj1i  32694  satffunlem  35764  frinfm  38246  filbcmb  38251  unichnidl  38542  dmncan1  38587  pclfinclN  40586  iccelpart  48037  prmdvdsfmtnof1lem2  48192  gpgcubic  48699  gpg5nbgr3star  48701  scmsuppss  49002  iscnrm3lem4  49565