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 370 | . 2 | |
3 | 1, 2 | sylib 127 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ralss 3006 rexss 3007 reuhypd 4203 elxp4 4808 elxp5 4809 dfco2a 4821 feu 5072 funbrfv2b 5218 dffn5im 5219 eqfnfv2 5266 dff4im 5313 fmptco 5330 dff13 5407 mpt2xopovel 5856 brtposg 5869 dftpos3 5877 erinxp 6180 qliftfun 6188 genpdflem 6605 ltexprlemm 6698 prime 8337 |
Copyright terms: Public domain | W3C validator |