![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr4i | GIF version |
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr4i.1 | ⊢ (𝜑 ↔ 𝜓) |
bitr4i.2 | ⊢ (𝜒 ↔ 𝜓) |
Ref | Expression |
---|---|
bitr4i | ⊢ (𝜑 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4i.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | bitr4i.2 | . . 3 ⊢ (𝜒 ↔ 𝜓) | |
3 | 2 | bicomi 132 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | bitri 184 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3bitr2i 208 3bitr2ri 209 3bitr4i 212 3bitr4ri 213 biancomi 270 imdistan 444 bianass 469 biadani 612 mpbiran 942 mpbiran2 943 3anrev 990 an6 1332 nfand 1579 19.33b2 1640 nf3 1680 nf4dc 1681 nf4r 1682 equsalh 1737 sb6x 1790 sb5f 1815 sbidm 1862 sb5 1899 sbanv 1901 sborv 1902 sbhb 1952 sb3an 1970 sbel2x 2010 sbal1yz 2013 sbexyz 2015 eu2 2082 2eu4 2131 cleqh 2289 cleqf 2357 dcne 2371 necon3bii 2398 ne3anior 2448 r2alf 2507 r2exf 2508 r19.23t 2597 r19.26-3 2620 r19.26m 2621 r19.43 2648 rabid2 2667 isset 2758 ralv 2769 rexv 2770 reuv 2771 rmov 2772 rexcom4b 2777 ceqsex4v 2795 ceqsex8v 2797 ceqsrexv 2882 ralrab2 2917 rexrab2 2919 reu2 2940 reu3 2942 reueq 2951 2reuswapdc 2956 reuind 2957 sbc3an 3039 rmo2ilem 3067 csbcow 3083 dfss2 3159 dfss3 3160 dfss3f 3162 ssabral 3241 rabss 3247 ssrabeq 3257 uniiunlem 3259 dfdif3 3260 ddifstab 3282 uncom 3294 inass 3360 indi 3397 difindiss 3404 difin2 3412 reupick3 3435 n0rf 3450 eq0 3456 eqv 3457 vss 3485 disj 3486 disj3 3490 undisj1 3495 undisj2 3496 exsnrex 3649 euabsn2 3676 euabsn 3677 prssg 3764 dfuni2 3826 unissb 3854 elint2 3866 ssint 3875 dfiin2g 3934 iunn0m 3962 iunxun 3981 iunxiun 3983 iinpw 3992 disjnim 4009 dftr2 4118 dftr5 4119 dftr3 4120 dftr4 4121 vnex 4149 inuni 4173 snelpw 4231 sspwb 4234 opelopabsb 4278 eusv2 4475 orddif 4564 onintexmid 4590 zfregfr 4591 tfi 4599 opthprc 4695 elxp3 4698 xpiundir 4703 elvv 4706 brinxp2 4711 relsn 4749 reliun 4765 inxp 4779 raliunxp 4786 rexiunxp 4787 cnvuni 4831 dm0rn0 4862 elrn 4888 ssdmres 4947 dfres2 4977 dfima2 4990 args 5015 cotr 5028 intasym 5031 asymref 5032 intirr 5033 cnv0 5050 xp11m 5085 cnvresima 5136 resco 5151 rnco 5153 coiun 5156 coass 5165 dfiota2 5197 dffun2 5245 dffun6f 5248 dffun4f 5251 dffun7 5262 dffun9 5264 funfn 5265 svrelfun 5300 imadiflem 5314 dffn2 5386 dffn3 5395 fintm 5420 dffn4 5463 dff1o4 5488 brprcneu 5527 eqfnfv3 5636 fnreseql 5647 fsn 5709 abrexco 5781 imaiun 5782 mpo2eqb 6007 elovmpo 6096 abexex 6152 releldm2 6211 fnmpo 6228 dftpos4 6289 tfrlem7 6343 0er 6594 eroveu 6653 erovlem 6654 map0e 6713 elixpconst 6733 domen 6778 reuen1 6828 xpf1o 6873 ssfilem 6904 finexdc 6931 pw1dc0el 6940 ssfirab 6963 sbthlemi10 6996 djuexb 7074 dmaddpq 7409 dmmulpq 7410 distrnqg 7417 enq0enq 7461 enq0tr 7464 nqnq0pi 7468 distrnq0 7489 prltlu 7517 prarloc 7533 genpdflem 7537 ltexprlemm 7630 ltexprlemlol 7632 ltexprlemupu 7634 ltexprlemdisj 7636 recexprlemdisj 7660 ltresr 7869 elnnz 9294 dfz2 9356 2rexuz 9614 eluz2b1 9633 elxr 9808 elixx1 9929 elioo2 9953 elioopnf 9999 elicopnf 10001 elfz1 10045 fzdifsuc 10113 fznn 10121 fzp1nel 10136 fznn0 10145 dfrp2 10296 redivap 10918 imdivap 10925 rexanre 11264 climreu 11340 prodmodc 11621 3dvdsdec 11905 3dvds2dec 11906 bezoutlembi 12041 nnwosdc 12075 isprm2 12152 isprm3 12153 isprm4 12154 pythagtriplem2 12301 elgz 12406 inffinp1 12483 isnsg4 13168 isrng 13305 isring 13371 dfrhm2 13521 lss1d 13716 isbasis3g 14023 restsn 14157 lmbr 14190 txbas 14235 tx2cn 14247 elcncf1di 14543 dedekindicclemicc 14587 limcrcl 14604 bj-nnor 14964 bj-vprc 15126 ss1oel2o 15222 subctctexmid 15229 trirec0xor 15272 |
Copyright terms: Public domain | W3C validator |