Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr3d | GIF version |
Description: Deduction form of bitr3i 185. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr3d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bitr3d.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
bitr3d | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | bicomd 140 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓)) |
3 | bitr3d.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | |
4 | 2, 3 | bitrd 187 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3bitrrd 214 3bitr3d 217 3bitr3rd 218 pm5.16 813 biassdc 1373 pm5.24dc 1376 anxordi 1378 sbequ12a 1746 drex1 1770 sbcomxyyz 1945 sb9v 1953 csbiebt 3039 prsspwg 3679 bnd2 4097 copsex2t 4167 copsex2g 4168 fnssresb 5235 fcnvres 5306 dmfco 5489 funimass5 5537 fmptco 5586 cbvfo 5686 cbvexfo 5687 isocnv 5712 isoini 5719 isoselem 5721 riota2df 5750 ovmpodxf 5896 caovcanrd 5934 fidcenumlemrks 6841 ordiso2 6920 ltpiord 7127 dfplpq2 7162 dfmpq2 7163 enqeceq 7167 enq0eceq 7245 enreceq 7544 ltpsrprg 7611 mappsrprg 7612 cnegexlem3 7939 subeq0 7988 negcon1 8014 subexsub 8134 subeqrev 8138 lesub 8203 ltsub13 8205 subge0 8237 div11ap 8460 divmuleqap 8477 ltmuldiv2 8633 lemuldiv2 8640 nn1suc 8739 addltmul 8956 elnnnn0 9020 znn0sub 9119 prime 9150 indstr 9388 qapne 9431 qlttri2 9433 fz1n 9824 fzrev3 9867 fzonlt0 9944 divfl0 10069 modqsubdir 10166 fzfig 10203 sqrt11 10811 sqrtsq2 10815 absdiflt 10864 absdifle 10865 nnabscl 10872 minclpr 11008 xrnegiso 11031 xrnegcon1d 11033 clim2 11052 climshft2 11075 sumrbdc 11148 prodrbdclem2 11342 sinbnd 11459 cosbnd 11460 dvdscmulr 11522 dvdsmulcr 11523 oddm1even 11572 qredeq 11777 cncongr2 11785 isprm3 11799 prmrp 11823 sqrt2irr 11840 crth 11900 eltg3 12226 eltop 12238 eltop2 12239 eltop3 12240 lmbrf 12384 cncnpi 12397 txcn 12444 hmeoimaf1o 12483 ismet2 12523 xmseq0 12637 |
Copyright terms: Public domain | W3C validator |