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 9298 indfval 9301 xaddval 10257 0tonninf 10890 1tonninf 10891 nninfinf 10893 sumeq1 12137 summodc 12166 zsumdc 12167 fsum3 12170 isumss 12174 sumsplitdc 12215 prodeq1f 12335 zproddc 12362 fprodseq 12366 nninfctlemfo 12833 pcmpt 13142 pcmpt2 13143 pcfac 13149 lgsval 16221 lgsneg 16241 lgsdilem 16244 lgsdir2 16250 lgsdir 16252 bj-charfunbi 16935 pw1map 17123 subctctexmid 17128 nninfalllem1 17149 nninfsellemdc 17151 nninfself 17154 nninfsellemeq 17155 nninfsellemqall 17156 nninfsellemeqinf 17157 nninfomni 17160 nninffeq 17161 nnnninfex 17163 dceqnconst 17208 dcapnconst 17209