ifbid - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ifbid		Unicode version

Theorem ifbid 3631

Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)

**Hypothesis**
Ref	Expression
ifbid.1

**Assertion**
Ref	Expression
ifbid

**Proof of Theorem ifbid**
Step	Hyp	Ref	Expression
1		ifbid.1	. 2
2		ifbi 3630	. 2
3	1, 2	syl 14	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1398

cif 3607

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-11 1555 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-ext 2213

This theorem depends on definitions: df-bi 117 df-tru 1401 df-nf 1510 df-sb 1811 df-clab 2218 df-cleq 2224 df-if 3608

This theorem is referenced by: ifbieq1d 3632 ifbieq2d 3634 ifbieq12d 3636 ifandc 3650 ifordc 3651 rabsnif 3742 suppsnopdc 6428 pw2f1odclem 7063 nnnninf 7385 nnnninf2 7386 nnnninfeq 7387 nninfisollemne 7390 nninfisol 7392 fodjum 7405 fodju0 7406 fodjuomni 7408 fodjumkv 7419 nninfwlporlemd 7431 nninfwlpor 7433 nninfwlpoimlemg 7434 nninfwlpoimlemginf 7435 nninfwlpoim 7438 nninfinfwlpo 7439 xaddval 10141 0tonninf 10765 1tonninf 10766 nninfinf 10768 sumeq1 11995 summodc 12024 zsumdc 12025 fsum3 12028 isumss 12032 sumsplitdc 12073 prodeq1f 12193 zproddc 12220 fprodseq 12224 nninfctlemfo 12691 pcmpt 12996 pcmpt2 12997 pcfac 13003 lgsval 15823 lgsneg 15843 lgsdilem 15846 lgsdir2 15852 lgsdir 15854 bj-charfunbi 16527 2omap 16715 pw1map 16717 subctctexmid 16722 nninfalllem1 16734 nninfsellemdc 16736 nninfself 16739 nninfsellemeq 16740 nninfsellemqall 16741 nninfsellemeqinf 16742 nninfomni 16745 nninffeq 16746 nnnninfex 16748 dceqnconst 16793 dcapnconst 16794