![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biimprcd | Structured version Visualization version GIF version |
Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
Ref | Expression |
---|---|
biimpcd.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
biimprcd | ⊢ (𝜒 → (𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜒 → 𝜒) | |
2 | biimpcd.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | syl5ibrcom 248 | 1 ⊢ (𝜒 → (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 |
This theorem is referenced by: biimparc 480 ax12i 1946 moanimlem 2671 euan 2674 euanv 2678 eleq1a 2878 ceqsalgALT 3473 cgsexg 3480 cgsex2g 3481 cgsex4g 3482 ceqsex 3483 spcegv 3540 spc2egv 3542 reu6 3651 csbiebt 3837 dfiin2g 4860 reusv2lem2 5191 ralxfrALT 5207 opelxp 5479 ssrel 5543 ssrel2 5545 ssrelrel 5555 iss 5784 ordun 6167 fprb 6823 riotaclb 7015 iunpw 7349 limom 7451 funcnvuni 7492 fiunlem 7499 soxp 7676 tfrlem8 7872 oaordex 8034 eroveu 8242 fundmen 8431 nneneq 8547 onfin2 8556 dif1en 8597 unfilem1 8628 rankwflemb 9068 sornom 9545 isf32lem9 9629 axdc3lem2 9719 axdc4lem 9723 zorn2lem3 9766 zorn2lem7 9770 tskuni 10051 grur1a 10087 grothomex 10097 genpnnp 10273 ltaddpr 10302 reclem4pr 10318 supadd 11457 supmullem1 11459 uzin 12127 elfzmlbp 12868 isfinite4 13573 brfi1uzind 13702 swrdnd 13852 sqrlem6 14441 sqreulem 14553 fvprmselgcd1 16210 lubun 17562 lspsneq 19584 fvmptnn04ifb 21143 fbasfip 22160 alexsubALTlem2 22340 ovolunlem1 23781 dchrisum0flb 25768 brbtwn2 26374 axcontlem8 26440 isclwwlknx 27501 clwwlknwwlksnb 27521 mdbr3 29765 mdbr4 29766 atssma 29846 atcvatlem 29853 ssrelf 30056 nepss 32556 sotr3 32610 nodmon 32766 noextendseq 32783 nocvxminlem 32856 hfun 33248 bj-ax12ig 33571 finxpreclem2 34202 indexdom 34541 fdc 34552 totbndss 34587 grpomndo 34685 iss2 35133 ax12eq 35608 ax12el 35609 lsatn0 35666 lsatcmp 35670 lsatcv0 35698 lfl1dim 35788 lfl1dim2N 35789 lkrss2N 35836 lub0N 35856 glb0N 35860 ispsubcl2N 36614 cdlemefrs29bpre0 37063 dihglblem2N 37961 dihglblem3N 37962 dochsnnz 38117 pm13.14 40279 tratrb 40409 ax6e2ndeq 40432 3impexpbicomVD 40730 tratrbVD 40734 equncomVD 40741 trsbcVD 40750 sbcssgVD 40756 csbingVD 40757 onfrALTVD 40764 csbsngVD 40766 csbxpgVD 40767 csbresgVD 40768 csbrngVD 40769 csbima12gALTVD 40770 csbunigVD 40771 csbfv12gALTVD 40772 con5VD 40773 hbimpgVD 40777 hbexgVD 40779 ax6e2ndeqVD 40782 supxrleubrnmpt 41221 suprleubrnmpt 41238 infxrgelbrnmpt 41272 isassintop 43595 zgtp1leeq 44057 |
Copyright terms: Public domain | W3C validator |