ifbid - Intuitionistic Logic Explorer

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

Theorem ifbid 3662

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

Colors of variables: wff set class

This proof depends on syntax axioms:

wi 4

wb 105

wceq 1402

cif 3638

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-11 1559 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-ext 2220

This proof depends on definitions: df-bi 117 df-tru 1405 df-nf 1514 df-sb 1816 df-clab 2225 df-cleq 2231 df-if 3639

This theorem is used by: ifbieq1d 3663 ifbieq2d 3665 ifbieq12d 3667 ifandc 3681 ifordc 3682 rabsnif 3778 suppsnopdc 6490 pw2f1odclem 7134 2omap 7318 nnnninf 7466 nnnninf2 7467 nnnninfeq 7468 nninfisollemne 7471 nninfisol 7473 fodjum 7486 fodju0 7487 fodjuomni 7489 fodjumkv 7500 nninfwlporlemd 7512 nninfwlpor 7514 nninfwlpoimlemg 7515 nninfwlpoimlemginf 7516 nninfwlpoim 7519 nninfinfwlpo 7520 indval 9296 indfval 9299 xaddval 10247 0tonninf 10877 1tonninf 10878 nninfinf 10880 sumeq1 12121 summodc 12150 zsumdc 12151 fsum3 12154 isumss 12158 sumsplitdc 12199 prodeq1f 12319 zproddc 12346 fprodseq 12350 nninfctlemfo 12817 pcmpt 13122 pcmpt2 13123 pcfac 13129 lgsval 16123 lgsneg 16143 lgsdilem 16146 lgsdir2 16152 lgsdir 16154 bj-charfunbi 16837 pw1map 17025 subctctexmid 17030 nninfalllem1 17051 nninfsellemdc 17053 nninfself 17056 nninfsellemeq 17057 nninfsellemqall 17058 nninfsellemeqinf 17059 nninfomni 17062 nninffeq 17063 nnnninfex 17065 dceqnconst 17110 dcapnconst 17111