Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > impbid | GIF version |
Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.) |
Ref | Expression |
---|---|
impbid.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
impbid.2 | ⊢ (𝜑 → (𝜒 → 𝜓)) |
Ref | Expression |
---|---|
impbid | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impbid.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | impbid.2 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜓)) | |
3 | 1, 2 | impbid21d 119 | . 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒))) |
4 | 3 | pm2.43i 43 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: bicom1 122 impbid1 130 pm5.74 168 imbi1d 220 pm5.501 233 pm5.32d 423 impbida 528 notbid 592 pm5.21 611 nbn2 613 2falsed 618 pm5.21ndd 621 orbi2d 704 con4biddc 754 con1bidc 768 con1bdc 772 oibabs 800 dedlema 876 dedlemb 877 xorbin 1275 albi 1357 19.21ht 1473 exbi 1495 19.23t 1567 equequ1 1598 equequ2 1599 elequ1 1600 elequ2 1601 equsexd 1617 dral1 1618 cbv2h 1634 sbequ12 1654 sbiedh 1670 drex1 1679 ax11b 1707 sbequ 1721 sbft 1728 sb56 1765 cbvexdh 1801 eupickb 1981 eupickbi 1982 ceqsalt 2580 ceqex 2671 mob2 2721 euxfr2dc 2726 reu6 2730 sbciegft 2793 eqsbc3r 2819 csbiebt 2886 sseq1 2966 reupick 3221 reupick2 3223 disjeq2 3749 disjeq1 3752 copsexg 3981 euotd 3991 poeq2 4037 sotritric 4061 sotritrieq 4062 seeq1 4076 seeq2 4077 alxfr 4193 ralxfrd 4194 rexxfrd 4195 ordelsuc 4231 sosng 4413 iss 4654 iotaval 4878 funeq 4921 funssres 4942 tz6.12c 5203 fnbrfvb 5214 ssimaex 5234 fvimacnv 5282 elpreima 5286 fsn 5335 fconst2g 5376 elunirn 5405 f1ocnvfvb 5420 foeqcnvco 5430 f1eqcocnv 5431 fliftfun 5436 isose 5460 isopo 5462 isoso 5464 f1oiso2 5466 eusvobj2 5498 oprabid 5537 f1opw2 5706 op1steq 5805 rntpos 5872 nnsucelsuc 6070 nnsucsssuc 6071 nnsseleq 6079 nnaord 6082 nnmord 6090 nnaordex 6100 nnawordex 6101 nnm00 6102 erexb 6131 swoord1 6135 swoord2 6136 iinerm 6178 fundmen 6286 nneneq 6320 nndomo 6326 fidifsnen 6331 ordiso2 6357 ordiso 6358 ltexnqq 6506 genprndl 6619 genprndu 6620 nqprl 6649 nqpru 6650 1idprl 6688 1idpru 6689 ltexprlemrnd 6703 ltaprg 6717 recexprlemrnd 6727 cauappcvgprlemrnd 6748 caucvgprlemrnd 6771 caucvgprprlemrnd 6799 ltxrlt 7085 lttri3 7098 ltadd2 7416 reapti 7570 apreap 7578 ltmul1 7583 apreim 7594 ltleap 7621 mulap0b 7636 apmul1 7764 lt2msq 7852 nnsub 7952 zltnle 8291 zleloe 8292 zrevaddcl 8295 zltp1le 8298 zapne 8315 nn0n0n1ge2b 8320 zdiv 8328 nneo 8341 zeo2 8344 qrevaddcl 8578 xltneg 8749 iccid 8794 fzn 8906 0fz1 8909 uzsplit 8954 fzm1 8962 fzrevral 8967 ssfzo12bi 9081 qltnle 9101 flqge 9124 frec2uzlt2d 9190 shftlem 9417 shftuz 9418 caucvgrelemcau 9579 sqrtsq 9642 abs00ap 9660 cau3lem 9710 climshft 9825 bj-notbi 10045 |
Copyright terms: Public domain | W3C validator |