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 29364

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 431	. . 3 $\/$
2		elim2ifim.1	. . . . 5
3	2	ancli 574	. . . 4 $/\$
4		pm4.42 1004	. . . . . 6 $/\$ $\/$ $/\$
5		elim2ifim.2	. . . . . . . . . 10 $/\$
6	5	ex 450	. . . . . . . . 9
7	6	ancld 576	. . . . . . . 8 $/\$
8	7	imp 445	. . . . . . 7 $/\$ $/\$
9		elim2ifim.3	. . . . . . . . . 10 $/\$
10	9	ex 450	. . . . . . . . 9
11	10	ancld 576	. . . . . . . 8 $/\$
12	11	imp 445	. . . . . . 7 $/\$ $/\$
13	8, 12	orim12i 538	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	4, 13	sylbi 207	. . . . 5 $/\$ $\/$ $/\$
15	14	ancli 574	. . . 4 $/\$ $/\$ $\/$ $/\$
16	3, 15	orim12i 538	. . 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 29363	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
22	17, 21	mpbir 221	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

cif 4086

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-if 4087

This theorem is referenced by: (None)