elim2ifim - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > elim2ifim		Structured version Visualization version Unicode version

Theorem elim2ifim 28210

Description: Elimination of two conditional operators for an implication. (Contributed by Thierry Arnoux, 25-Jan-2017.)

**Assertion**
Ref	Expression
elim2ifim

**Proof of Theorem elim2ifim**
Step	Hyp	Ref	Expression
1		exmid 421	. . 3 $\/$
2		elim2ifim.1	. . . . 5
3	2	ancli 558	. . . 4 $/\$
4		pm4.42 977	. . . . . 6 $/\$ $\/$ $/\$
5		elim2ifim.2	. . . . . . . . . 10 $/\$
6	5	ex 440	. . . . . . . . 9
7	6	ancld 560	. . . . . . . 8 $/\$
8	7	imp 435	. . . . . . 7 $/\$ $/\$
9		elim2ifim.3	. . . . . . . . . 10 $/\$
10	9	ex 440	. . . . . . . . 9
11	10	ancld 560	. . . . . . . 8 $/\$
12	11	imp 435	. . . . . . 7 $/\$ $/\$
13	8, 12	orim12i 523	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	4, 13	sylbi 200	. . . . 5 $/\$ $\/$ $/\$
15	14	ancli 558	. . . 4 $/\$ $/\$ $\/$ $/\$
16	3, 15	orim12i 523	. . 3 $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
17	1, 16	ax-mp 5	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
18		elim2if.1	. . 3
19		elim2if.2	. . 3
20		elim2if.3	. . 3
21	18, 19, 20	elim2if 28209	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
22	17, 21	mpbir 214	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 374 $/\$ wa 375

wceq 1454

cif 3892

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-if 3893

This theorem is referenced by: (None)