con4 - Metamath Proof Explorer

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

Theorem con4 112

Description: Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 113 and its associated deduction is con4d 114. (Contributed by BJ, 24-Dec-2020.)

**Assertion**
Ref	Expression
con4

**Proof of Theorem con4**
Step	Hyp	Ref	Expression
1		ax-3 8	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

This theorem was proved from axioms: ax-3 8

This theorem is referenced by: con4i 113 con4d 114 con34b 306 meredith 1566 bj-con4iALT 32547 bj-alcomexcom 32670 frege54cor0a 38157 notnotrALTVD 39151 con3ALTVD 39152

W3C validator