![]() |
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 591 pm5.21 610 nbn2 612 2falsed 617 pm5.21ndd 620 orbi2d 703 con4biddc 753 con1bidc 767 con1bdc 771 oibabs 799 dedlema 875 dedlemb 876 xorbin 1272 albi 1354 19.21ht 1470 exbi 1492 19.23t 1564 equequ1 1595 equequ2 1596 elequ1 1597 elequ2 1598 equsexd 1614 dral1 1615 cbv2h 1631 sbequ12 1651 sbiedh 1667 drex1 1676 ax11b 1704 sbequ 1718 sbft 1725 sb56 1762 cbvexdh 1798 eupickb 1978 eupickbi 1979 ceqsalt 2574 ceqex 2665 mob2 2715 euxfr2dc 2720 reu6 2724 sbciegft 2787 eqsbc3r 2813 csbiebt 2880 sseq1 2960 reupick 3215 reupick2 3217 disjeq2 3740 disjeq1 3743 copsexg 3972 euotd 3982 poeq2 4028 sotritric 4052 sotritrieq 4053 seeq1 4061 seeq2 4062 alxfr 4159 ralxfrd 4160 rexxfrd 4161 ordelsuc 4197 sosng 4356 iss 4597 iotaval 4821 funeq 4864 funssres 4885 tz6.12c 5146 fnbrfvb 5157 ssimaex 5177 fvimacnv 5225 elpreima 5229 fsn 5278 fconst2g 5319 elunirn 5348 f1ocnvfvb 5363 foeqcnvco 5373 f1eqcocnv 5374 fliftfun 5379 isose 5403 isopo 5405 isoso 5407 f1oiso2 5409 eusvobj2 5441 oprabid 5480 f1opw2 5648 op1steq 5747 rntpos 5813 nnsucelsuc 6009 nnsucsssuc 6010 nnaord 6018 nnmord 6026 nnaordex 6036 nnawordex 6037 nnm00 6038 erexb 6067 swoord1 6071 swoord2 6072 iinerm 6114 fundmen 6222 ltexnqq 6391 genprndl 6504 genprndu 6505 nqprl 6533 1idprl 6566 1idpru 6567 ltexprlemrnd 6579 ltaprg 6592 recexprlemrnd 6601 cauappcvgprlemrnd 6622 caucvgprlemrnd 6644 ltxrlt 6882 lttri3 6895 ltadd2 7212 reapti 7363 apreap 7371 ltmul1 7376 apreim 7387 ltleap 7413 mulap0b 7418 apmul1 7546 lt2msq 7633 nnsub 7733 zltnle 8067 zleloe 8068 zrevaddcl 8071 zltp1le 8074 zapne 8091 nn0n0n1ge2b 8096 zdiv 8104 nneo 8117 zeo2 8120 qrevaddcl 8353 xltneg 8519 iccid 8564 fzn 8676 0fz1 8679 uzsplit 8724 fzm1 8732 fzrevral 8737 ssfzo12bi 8851 frec2uzlt2d 8871 sqrtsq 9214 bj-notbi 9380 |
Copyright terms: Public domain | W3C validator |