ifbid - Intuitionistic Logic Explorer

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

Theorem ifbid 3644

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 3643	. 2
3	1, 2	syl 14	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1398

cif 3620

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 2214

This theorem depends on definitions: df-bi 117 df-tru 1401 df-nf 1510 df-sb 1812 df-clab 2219 df-cleq 2225 df-if 3621

This theorem is referenced by: ifbieq1d 3645 ifbieq2d 3647 ifbieq12d 3649 ifandc 3663 ifordc 3664 rabsnif 3758 suppsnopdc 6450 pw2f1odclem 7087 2omap 7269 nnnninf 7417 nnnninf2 7418 nnnninfeq 7419 nninfisollemne 7422 nninfisol 7424 fodjum 7437 fodju0 7438 fodjuomni 7440 fodjumkv 7451 nninfwlporlemd 7463 nninfwlpor 7465 nninfwlpoimlemg 7466 nninfwlpoimlemginf 7467 nninfwlpoim 7470 nninfinfwlpo 7471 xaddval 10178 0tonninf 10802 1tonninf 10803 nninfinf 10805 sumeq1 12040 summodc 12069 zsumdc 12070 fsum3 12073 isumss 12077 sumsplitdc 12118 prodeq1f 12238 zproddc 12265 fprodseq 12269 nninfctlemfo 12736 pcmpt 13041 pcmpt2 13042 pcfac 13048 lgsval 15877 lgsneg 15897 lgsdilem 15900 lgsdir2 15906 lgsdir 15908 bj-charfunbi 16581 pw1map 16769 subctctexmid 16774 nninfalllem1 16786 nninfsellemdc 16788 nninfself 16791 nninfsellemeq 16792 nninfsellemqall 16793 nninfsellemeqinf 16794 nninfomni 16797 nninffeq 16798 nnnninfex 16800 dceqnconst 16846 dcapnconst 16847