3simp1i - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem 3simp1i 790

Description: Infer a conjunct from a triple conjunction.

**Hypothesis**
Ref	Expression
3simp1i.1	$/\$ $/\$

**Assertion**
Ref	Expression
3simp1i

**Proof of Theorem 3simp1i**
Step	Hyp	Ref	Expression
1		3simp1i.1	. 2 $/\$ $/\$
2		3simp1 787	. 2 $/\$ $/\$
3	1, 2	ax-mp 7	1

Colors of variables: wff set class

Syntax hints: $/\$ w3a 774

This theorem is referenced by: find 3150 sqrlem20 6630 bcpasc2t 6914 expcnvlem2 7171 expcnvlem4 7173 ivthlem6 7229 ivthlem7 7230 ivthlem8 7231 ivthlem6OLD 7238 ivthlem7OLD 7239 ivthlem8OLD 7240 ef01tllem2 7334 eflegeot 7364 efm1legeot 7366 siilem2 8456 pilem2 8610 pilem3 8611 pire 8615 pipos 8616 cosh111t 8651 efghgrpilem 8653 efifolem1 8656 efifolem2 8657 efif1lem5 8668 h2hva 8782 elunop2t 9876

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7

This theorem depends on definitions: df-bi 147 df-an 225 df-3an 776