Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm4.71rd | Unicode version |
Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.) |
Ref | Expression |
---|---|
pm4.71rd.1 |
Ref | Expression |
---|---|
pm4.71rd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71rd.1 | . 2 | |
2 | pm4.71r 387 | . 2 | |
3 | 1, 2 | sylib 121 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ralss 3133 rexss 3134 reuhypd 4362 elxp4 4996 elxp5 4997 dfco2a 5009 feu 5275 funbrfv2b 5434 dffn5im 5435 eqfnfv2 5487 dff4im 5534 fmptco 5554 dff13 5637 f1od2 6100 mpoxopovel 6106 brtposg 6119 dftpos3 6127 erinxp 6471 qliftfun 6479 genpdflem 7283 ltexprlemm 7376 prime 9118 oddnn02np1 11504 oddge22np1 11505 evennn02n 11506 evennn2n 11507 bastop2 12180 restopn2 12279 restdis 12280 tx1cn 12365 tx2cn 12366 imasnopn 12395 xmeter 12532 |
Copyright terms: Public domain | W3C validator |