Theorem iaci 36

Description: & introduction rule. Inference form of ax-iac 32.

Hypotheses

Ref	Expression
iaci.1	⊦ 𝜑
iaci.2	⊦ 𝜓

Assertion

Ref	Expression
iaci	⊦ (𝜑 & 𝜓)

Proof of Theorem iaci

Step	Hyp	Ref	Expression
1		iaci.1	. . . 4 ⊦ 𝜑
2	1	ax-ibot 4	. . 3 ⊦ (⊥ ⅋ 𝜑)
3		iaci.2	. . . 4 ⊦ 𝜓
4	3	ax-ibot 4	. . 3 ⊦ (⊥ ⅋ 𝜓)
5	2, 4	iac 35	. 2 ⊦ (⊥ ⅋ (𝜑 & 𝜓))
6	5	ax-ebot 5	1 ⊦ (𝜑 & 𝜓)

Syntax hints:  ⊥wbot 1   & wac 30

This theorem was proved from axioms:  ax-ibot 4  ax-ebot 5  ax-cut 6  ax-init 7  ax-mdco 8  ax-iac 32

This theorem is referenced by:  dflb  93  ilb  96  abs1  178