imp43 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > imp43		Structured version Visualization version GIF version

Theorem imp43 426

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 420	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	imp 405	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394

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 395

This theorem is referenced by: fundmen 9060 fiint 9354 ltexprlem6 11070 divgt0 12118 divge0 12119 le2sq2 14137 iscatd 17658 isfuncd 17856 islmodd 20754 lmodvsghm 20811 islssd 20824 basis2 22872 neindisj 23039 dvidlem 25862 spansneleq 31398 elspansn4 31401 adjmul 31920 kbass6 31949 mdsl0 32138 chirredlem1 32218 poimirlem29 37127 rngonegmn1r 37420 3dim1 38944 linepsubN 39229 pmapsub 39245 tgoldbach 47159

	
		OSZAR »