Theorem imp43 427

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 421	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	imp 406	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 206  df-an 396

This theorem is referenced by:  fundmen  8791  fiint  9052  ltexprlem6  10781  divgt0  11826  divge0  11827  le2sq2  13835  iscatd  17363  isfuncd  17561  islmodd  20110  lmodvsghm  20165  islssd  20178  basis2  22082  neindisj  22249  dvidlem  25060  spansneleq  29911  elspansn4  29914  adjmul  30433  kbass6  30462  mdsl0  30651  chirredlem1  30731  poimirlem29  35785  rngonegmn1r  36079  3dim1  37460  linepsubN  37745  pmapsub  37761  tgoldbach  45221