![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr4d | GIF version |
Description: Deduction form of bitr4i 187. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr4d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bitr4d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
Ref | Expression |
---|---|
bitr4d | ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | bitr4d.2 | . . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) | |
3 | 2 | bicomd 141 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
4 | 1, 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: 3bitr2d 216 3bitr2rd 217 3bitr4d 220 3bitr4rd 221 mpbirand 441 mpbiran2d 442 bianabs 611 imordc 898 3anibar 1167 xor2dc 1401 bilukdc 1407 reuhypd 4489 opelresi 4936 iota1 5210 funbrfv2b 5581 dffn5im 5582 fneqeql 5645 f1ompt 5688 dff13 5790 fliftcnv 5817 isotr 5838 isoini 5840 caovord3 6070 releldm2 6210 tpostpos 6289 nnsssuc 6527 nnaordi 6533 iserd 6585 ecdmn0m 6603 qliftel 6641 qliftfun 6643 qliftf 6646 ecopovsym 6657 pw2f1odclem 6862 mapen 6874 supisolem 7037 cnvti 7048 omp1eomlem 7123 ctssdc 7142 isomnimap 7165 ismkvmap 7182 iswomnimap 7194 netap 7283 2omotaplemap 7286 recmulnqg 7420 nqtri3or 7425 ltmnqg 7430 mullocprlem 7599 addextpr 7650 gt0srpr 7777 ltsosr 7793 ltasrg 7799 map2psrprg 7834 xrlenlt 8052 letri3 8068 subadd 8190 ltsubadd2 8420 lesubadd2 8422 suble 8427 ltsub23 8429 ltaddpos2 8440 ltsubpos 8441 subge02 8465 ltaddsublt 8558 reapneg 8584 apsym 8593 apti 8609 leltap 8612 ap0gt0 8627 divmulap 8662 divmulap3 8664 rec11rap 8698 ltdiv1 8855 ltdivmul2 8865 ledivmul2 8867 ltrec 8870 suprleubex 8941 nnle1eq1 8973 avgle1 9189 avgle2 9190 nn0le0eq0 9234 znnnlt1 9331 zleltp1 9338 elz2 9354 uzm1 9588 uzin 9590 difrp 9722 xrletri3 9834 xgepnf 9846 xltnegi 9865 xltadd1 9906 xposdif 9912 xleaddadd 9917 elioo5 9963 elfz5 10047 fzdifsuc 10111 elfzm11 10121 uzsplit 10122 elfzonelfzo 10260 qtri3or 10273 qavgle 10289 flqbi 10321 flqbi2 10322 zmodid2 10383 q2submod 10416 sqap0 10618 lt2sq 10625 le2sq 10626 nn0opthlem1d 10732 bcval5 10775 zfz1isolemiso 10851 shftfib 10864 mulreap 10905 caucvgrelemcau 11021 caucvgre 11022 elicc4abs 11135 abs2difabs 11149 cau4 11157 maxclpr 11263 negfi 11268 lemininf 11274 mul0inf 11281 xrlemininf 11311 xrminltinf 11312 clim2 11323 climeq 11339 fisumss 11432 fsumabs 11505 isumshft 11530 absefib 11810 dvdsval3 11830 dvdslelemd 11881 dvdsabseq 11885 dvdsflip 11889 dvdsssfz1 11890 zeo3 11905 ndvdsadd 11968 dvdssq 12064 algcvgblem 12081 lcmdvds 12111 ncoprmgcdgt1b 12122 isprm3 12150 phiprmpw 12254 prmdiv 12267 pc11 12363 pcz 12364 pockthlem 12388 1arith 12399 ercpbllemg 12806 grpinvcnv 13012 eqger 13163 ablsubadd 13251 dvdsr02 13455 opprunitd 13460 unitsubm 13469 issubrg3 13594 aprval 13598 rnglidlmmgm 13812 discld 14096 isneip 14106 restopnb 14141 restopn2 14143 restdis 14144 lmbr2 14174 cnptoprest 14199 cnptoprest2 14200 tx1cn 14229 tx2cn 14230 txcnmpt 14233 txrest 14236 elbl2ps 14352 elbl2 14353 blcomps 14356 blcom 14357 xblpnfps 14358 xblpnf 14359 blpnf 14360 xmeter 14396 bdxmet 14461 metrest 14466 xmetxp 14467 metcn 14474 cncfcdm 14529 reefiso 14658 m1lgs 14913 2lgsoddprmlem2 14915 |
Copyright terms: Public domain | W3C validator |