![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr3d | GIF version |
Description: Deduction form of bitr3i 186. (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 141 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓)) |
3 | bitr3d.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | |
4 | 2, 3 | bitrd 188 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ 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: 3bitrrd 215 3bitr3d 218 3bitr3rd 219 pm5.16 829 biassdc 1406 pm5.24dc 1409 anxordi 1411 sbequ12a 1784 drex1 1809 sbcomxyyz 1984 sb9v 1990 csbiebt 3111 prsspwg 3767 bnd2 4188 copsex2t 4260 copsex2g 4261 fnssresb 5344 fcnvres 5415 foelcdmi 5585 dmfco 5601 funimass5 5650 fmptco 5699 cbvfo 5803 cbvexfo 5804 isocnv 5829 isoini 5836 isoselem 5838 riota2df 5868 ovmpodxf 6018 caovcanrd 6056 fidcenumlemrks 6977 ordiso2 7059 ltpiord 7343 dfplpq2 7378 dfmpq2 7379 enqeceq 7383 enq0eceq 7461 enreceq 7760 ltpsrprg 7827 mappsrprg 7828 cnegexlem3 8159 subeq0 8208 negcon1 8234 subexsub 8354 subeqrev 8358 lesub 8423 ltsub13 8425 subge0 8457 div11ap 8682 divmuleqap 8699 ltmuldiv2 8857 lemuldiv2 8864 nn1suc 8963 addltmul 9180 elnnnn0 9244 znn0sub 9343 prime 9377 indstr 9618 qapne 9664 qlttri2 9666 fz1n 10069 fzrev3 10112 fzonlt0 10192 divfl0 10322 modqsubdir 10419 fzfig 10456 sqrt11 11075 sqrtsq2 11079 absdiflt 11128 absdifle 11129 nnabscl 11136 minclpr 11272 xrnegiso 11297 xrnegcon1d 11299 clim2 11318 climshft2 11341 sumrbdc 11414 prodrbdclem2 11608 fprodssdc 11625 sinbnd 11787 cosbnd 11788 dvdscmulr 11854 dvdsmulcr 11855 oddm1even 11907 qredeq 12123 cncongr2 12131 isprm3 12145 prmrp 12172 sqrt2irr 12189 crth 12251 pcdvdsb 12347 ssnnctlemct 12492 xpsfrnel2 12815 grpid 12976 grpidrcan 13002 grpidlcan 13003 grplmulf1o 13011 imasgrp2 13045 ghmeqker 13203 abladdsub4 13246 imasrng 13303 imasring 13407 lspsnss2 13728 eltg3 13994 eltop 14006 eltop2 14007 eltop3 14008 lmbrf 14152 cncnpi 14165 txcn 14212 hmeoimaf1o 14251 ismet2 14291 xmseq0 14405 lgsne0 14876 2sqlem7 14905 |
Copyright terms: Public domain | W3C validator |