Theorem imp43 428

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
imp43	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Proof of Theorem imp43

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	imp4b 422	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	imp 407	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 206  df-an 397

This theorem is referenced by:  fundmen  9011  fiint  9304  ltexprlem6  11015  divgt0  12061  divge0  12062  le2sq2  14079  iscatd  17596  isfuncd  17794  islmodd  20421  lmodvsghm  20477  islssd  20490  basis2  22378  neindisj  22545  dvidlem  25356  spansneleq  30681  elspansn4  30684  adjmul  31203  kbass6  31232  mdsl0  31421  chirredlem1  31501  poimirlem29  36305  rngonegmn1r  36599  3dim1  38127  linepsubN  38412  pmapsub  38428  tgoldbach  46243