ifbid - Intuitionistic Logic Explorer

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

Theorem ifbid 3659

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

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1402

cif 3635

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 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 theorem depends on definitions: df-bi 117 df-tru 1405 df-nf 1514 df-sb 1816 df-clab 2225 df-cleq 2231 df-if 3636

This theorem is referenced by: ifbieq1d 3660 ifbieq2d 3662 ifbieq12d 3664 ifandc 3678 ifordc 3679 rabsnif 3774 suppsnopdc 6480 pw2f1odclem 7124 2omap 7308 nnnninf 7456 nnnninf2 7457 nnnninfeq 7458 nninfisollemne 7461 nninfisol 7463 fodjum 7476 fodju0 7477 fodjuomni 7479 fodjumkv 7490 nninfwlporlemd 7502 nninfwlpor 7504 nninfwlpoimlemg 7505 nninfwlpoimlemginf 7506 nninfwlpoim 7509 nninfinfwlpo 7510 xaddval 10226 0tonninf 10855 1tonninf 10856 nninfinf 10858 sumeq1 12099 summodc 12128 zsumdc 12129 fsum3 12132 isumss 12136 sumsplitdc 12177 prodeq1f 12297 zproddc 12324 fprodseq 12328 nninfctlemfo 12795 pcmpt 13100 pcmpt2 13101 pcfac 13107 lgsval 16037 lgsneg 16057 lgsdilem 16060 lgsdir2 16066 lgsdir 16068 bj-charfunbi 16751 pw1map 16939 subctctexmid 16944 nninfalllem1 16956 nninfsellemdc 16958 nninfself 16961 nninfsellemeq 16962 nninfsellemqall 16963 nninfsellemeqinf 16964 nninfomni 16967 nninffeq 16968 nnnninfex 16970 dceqnconst 17015 dcapnconst 17016