ifbid - Intuitionistic Logic Explorer

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

Theorem ifbid 3648

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

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1398

cif 3624

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 2216

This theorem depends on definitions: df-bi 117 df-tru 1401 df-nf 1510 df-sb 1812 df-clab 2221 df-cleq 2227 df-if 3625

This theorem is referenced by: ifbieq1d 3649 ifbieq2d 3651 ifbieq12d 3653 ifandc 3667 ifordc 3668 rabsnif 3763 suppsnopdc 6463 pw2f1odclem 7100 2omap 7282 nnnninf 7430 nnnninf2 7431 nnnninfeq 7432 nninfisollemne 7435 nninfisol 7437 fodjum 7450 fodju0 7451 fodjuomni 7453 fodjumkv 7464 nninfwlporlemd 7476 nninfwlpor 7478 nninfwlpoimlemg 7479 nninfwlpoimlemginf 7480 nninfwlpoim 7483 nninfinfwlpo 7484 xaddval 10197 0tonninf 10826 1tonninf 10827 nninfinf 10829 sumeq1 12065 summodc 12094 zsumdc 12095 fsum3 12098 isumss 12102 sumsplitdc 12143 prodeq1f 12263 zproddc 12290 fprodseq 12294 nninfctlemfo 12761 pcmpt 13066 pcmpt2 13067 pcfac 13073 lgsval 16003 lgsneg 16023 lgsdilem 16026 lgsdir2 16032 lgsdir 16034 bj-charfunbi 16707 pw1map 16895 subctctexmid 16900 nninfalllem1 16912 nninfsellemdc 16914 nninfself 16917 nninfsellemeq 16918 nninfsellemqall 16919 nninfsellemeqinf 16920 nninfomni 16923 nninffeq 16924 nnnninfex 16926 dceqnconst 16972 dcapnconst 16973