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 7319 nnnninf 7467 nnnninf2 7468 nnnninfeq 7469 nninfisollemne 7472 nninfisol 7474 fodjum 7487 fodju0 7488 fodjuomni 7490 fodjumkv 7501 nninfwlporlemd 7513 nninfwlpor 7515 nninfwlpoimlemg 7516 nninfwlpoimlemginf 7517 nninfwlpoim 7520 nninfinfwlpo 7521 indval 9299 indfval 9302 xaddval 10258 0tonninf 10892 1tonninf 10893 nninfinf 10895 sumeq1 12140 summodc 12169 zsumdc 12170 fsum3 12173 isumss 12177 sumsplitdc 12218 prodeq1f 12338 zproddc 12365 fprodseq 12369 nninfctlemfo 12836 pcmpt 13145 pcmpt2 13146 pcfac 13152 prmorcht 16243 lgsval 16289 lgsneg 16309 lgsdilem 16312 lgsdir2 16318 lgsdir 16320 bj-charfunbi 17003 pw1map 17191 subctctexmid 17196 nninfalllem1 17217 nninfsellemdc 17219 nninfself 17222 nninfsellemeq 17223 nninfsellemqall 17224 nninfsellemeqinf 17225 nninfomni 17228 nninffeq 17229 nnnninfex 17231 dceqnconst 17277 dcapnconst 17278