ad5antlr - Metamath Proof Explorer

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

Theorem ad5antlr 734

Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

**Hypothesis**
Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

**Assertion**
Ref	Expression
ad5antlr	⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

**Proof of Theorem ad5antlr**
Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad4antr 731	1 ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Colors of variables: wff setvar class

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: simp-5r 785 fimaproj 8134 restmetu 24472 foresf1o 32293 2ndresdju 32428 nn0xmulclb 32535 isdrng4 32956 fracfld 32988 elrspunidl 33138 elrspunsn 33139 rhmpreimaprmidl 33161 fedgmul 33319 locfinreflem 33435 pstmxmet 33492 satfdmlem 34972 mblfinlem3 37126 itg2gt0cn 37142 dffltz 42052 pell1234qrmulcl 42269 suplesup 44715 limclner 45033 bgoldbtbnd 47143 gricushgr 47177

W3C validator

	
		OSZAR »